Metamath and the Peano Induction Axiom

In email, someone pointed me at an automated proof system called [Metamath][metamath]. Metamath generates proofs of mathematical statements using ZF set theory. The proofs are actually relatively easy to follow, which is quite unusual for an automated theorem prover. I’ll definitely write more about Metamath some other time, but I thought it would be interesting today to point to [metamaths proof of the fifth axiom of Peano arithmetic][meta-peano], the principle of induction. Here’s a screenshot of the first 15 steps; following the link to see the whole thing.
peano5-proof.jpg
[metamath]: http://us.metamath.org/mpegif/mmset.html#overview
[meta-peano]: http://us.metamath.org/mpegif/peano5.html

0 thoughts on “Metamath and the Peano Induction Axiom

  1. Slawekk

    Metamath is a proof verifier, so it does not generate proofs. Proofs are written by a human in the Metamath language and then verified by Metamath (the verifier).
    Metamath can generate views of the proofs in different formats, like the one above.
    It would be very nice to have a real theorem prover for Metamath with a language interface similar to Isar

    Reply

Leave a Reply