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 tr

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 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."