As discussed in the Proof Explorer page, the Metamath proof that "2+2=4" has 26,323 steps.
The reason for such a long proof is Metamath first defines the real and the complex numbers. There are good reasons to do so. However, I would like to check the proof that "2+2=4" using basic ZFC, which would probably result in a shorter proof. I see there is another proof (the one of Principia Mathematica), but I think (but I am not 100% sure) that this proof is not the simple one I am looking for. Has a simple proof for "2+2=4" been written in metamath? Thank you in advance. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/125a62b7-97ee-4e26-bbe9-f72e5e60abd3n%40googlegroups.com.
