Right. That seems like an unnecessary detour to me.

It's necessary to go down to the level of axioms and do one step at a time. It's obviously not needed for us to see that this proof is correct.

A human proof would probably not generally go beyond something like:

2+2=4

1+1+1+1 = 1+1+1+1 // Substitute the definitions of 2 (1+1) and 4 (1+1+1+1)

Except that 4 is not 1+1+1+1, it's the successor of 3, which is the successor of 2 which is the successor of 1 which is the successor of 0. So you'd have to show that:

S(S(0)) + S(S(0)) = S(S(S(S(0))))

and that is non-trivial. (But it's not 26,000 steps either.)

It is trivial in most axiomatic systems. It’s directly linked to how + is defined and will mostly boil down to applying it. The 26000 steps proof is extremely convoluted.

I'm assuming those steps in the definitions of 2 and 4, but you're right that this is part of why it gets so tedious.