"The complete proof of 2 + 2 = 4 involves 2,863 subtheorems including the 189 above. (The command "show trace_back 2p2e4 /essential" will list them.) 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." http://us.metamath.org/mpegif/mmset.html#trivia