It's not so much to prove that 1+1=2; rather to set up the definitions and background entirely from scratch. If you had to define the grammar and vocabulary of English before you wrote a sonnet, your sonnets too would be exceedingly long.
Exactly right. Most of those background steps do things like establish the basics of complex numbers, and you can reuse them for anything else involving complex numbers.
It is only 10 steps long. Yes, it is longer than an informal proof (such as one printed in a math journal), but it is not hard to follow. In this case this proof is rigorously verified by four different independent computer verifiers all the way back to the axioms of logic and set theory.
It is already possible to have proofs that are completely computer verified. Up to this point, mathematicians often do not use them because it is simpler not to. But in the long-term, I think we should change our expectations to start requiring proofs to be verified by computer if we really want to believe in them. Humans make mistakes, and reviewers often miss them. Computer verification, especially when there are multiple independent verifiers, provide much greater confidence that the claimed proof is actually correct. The number of so-called proofs that are actually not proofs is very large.
