In email, someone pointed me at an automated proof system called 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, the principle of induction. Here's a screenshot of the first 15 steps; following the link to see the whole thing.
Comments
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...
Posted by: Slawekk | August 10, 2006 12:36 PM
Ooh, I tried to read that, but all those characters got too swimmy -- Pro mea lingua Graeca est!
Posted by: andrea | August 10, 2006 2:18 PM
Quidquidne lingua Latina dictum altum videtur, Andrea?
Posted by: Thomas Winwood | August 11, 2006 10:39 AM