> … a total of 26,323 steps—this is how many steps you would have to examine if you wanted to verify the proof by hand in complete detail all the way back to the axioms of ZFC set theory

I can’t help but shake the feeling that if it takes this many steps to prove 2+2=4 then you’ve done something wrong in the design of your formalism.

> One of the reasons that the proof of 2 + 2 = 4 is so long is that 2 and 4 are complex numbers—i.e. we are really proving (2+0i) + (2+0i) = (4+0i)

Yeah, this is why

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.