3 ms·
"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
by mazsa 9y ago
"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 http://us.metamath.org/mpegif/mmset.html#trivia
- komali2 9y agoJesus! I guess I'll just stick to 2+2 holy shit this is well beyond me! Thanks for the link. EDIT: Nope guess not now I'm knee deep in this thing :P
- ulucs 9y agoOh jeez dude, just use ZFC and you'll get it done in ten minutes
- Avshalom 9y agoWell that's precisely the point, if you pick your axioms/theorems/lemma's right you get to skip a lot of steps and only calculate a particular end result instead of every turtle along the way.