Hi, playing with my code to build Metamath proofs from ITP programs, I generated this proof of the theorem asserting that each group where all elements have order 2 is commutative:
https://github.com/giomasce/set.mm/commit/6b64e8068b1c1c82d2fb714c42ae2615bee80094 I thought anyone having a fetish for monster Metamath proofs might like it. You can also find the HTML rendering here (25 MB, be careful!): https://people.debian.org/~gio/monsterord2com.html This is the description, with some additional explanation on why it is so big and weird: --- A monster theorem, proving that a group where every element has order 2 (i.e., every element multiplied by itself is the identity) is commutative. The proof is automatically generated: the original problem is fed as a First-Order Formula to Prover9, whose proof is processed with GAPT to convert it to Natural Deduction style. The program mmpp is finally used to express the proof in the Metamath language. Since the original theorem is not completely trivial itself and each conversion step adds a good amount of bookkeeping code, the final result is huge and hardly readable by any human being. The statement itself is littered with artifacts due to the automatic conversion from a First Order Formula. The class 𝐴 is the group identity and the class 𝐵 (depending on variables 𝑡 and 𝑒) is the group operation. Explicit substitution is used both in the statement and in the proof in order to bridge the gap between FOF and Metamath's treating of predicates' and functors' arguments: while in First Order Formulae arguments are explicit and order-based, in Metamath they are implicit and name-based. A conspicuous amount of bookkeeping must be put in place to handle this discrepancy. --- BTW, the proof generated by mmpp is uncompressed. Compressing with with metamath.exe took a few good minutes. Giovanni. -- Giovanni Mascellani <[email protected]> Postdoc researcher - Université Libre de Bruxelles -- 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/5c9541be-26a8-532d-d571-e2f5765db4fb%40gmail.com.
signature.asc
Description: OpenPGP digital signature
