Someone already linked metamath, it also gives a flavor of just how long some proofs can be when you fully formalize them and start from ZFC axioms. From the trivia page at http://us.metamath.org/mpeuni/mmset.html#trivia "The complete proof of [(2+0i) + (2+0i) = (4+0i)] involves 2,863 subtheorems including the 189 above. These have a total of 27,426 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."

Depends on your starting point. You can prove 1+1=2 quite easily from the Peano axioms:

1+1=1+S(0) [definition of 1]

1+S(0)=S(1+0) [definition of addition, a+S(b)=S(a+b)]

1+1=S(1+0) [transitivity of equality]

S(1+0)=S(1) [definition of addition, a+0=a]

1+1=S(1) [transitivity of equality]

S(1)=2 [definition of 2]

1+1=2 [transitivity of equality]

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.

The actual proof in metamath that two plus two is equal to 4 is at http://us.metamath.org/mpeuni/2p2e4.html

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.

If you are curious about metamath, I have a video on YouTube that you might find interesting: https://m.youtube.com/watch?v=8WH4Rd4UKGE#

It's like telling that there are thousands of machine instructions to be able to write printf("%.2f", x). It means that we should use the power of abstraction.

That was exactly the point, if you abstract then you are handwaving details (unless you abstract inside a formal system that itself defines methods for abstraction and then you are back to square one)