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.
[metamath]: http://us.metamath.org/mpegif/mmset.html#overview
[meta-peano]: http://us.metamath.org/mpegif/peano5.html
Good Math/Bad Math
The beauty of math; the humor of stupidity.
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…
Ooh, I tried to read that, but all those characters got too swimmy — Pro mea lingua Graeca est!
Quidquidne lingua Latina dictum altum videtur, Andrea?