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
- Log in to post comments
More like this
There was an interesting discussion about mathematical constructions in the comment thread on my post about the professor who doesn't like infinity, and I thought it was worth turning it into a post of its own.
In the history of this blog, I've often talked about the idea of "building mathematics…
Sorry for the delay in the category theory articles. I've been busy with work, and haven't had time to do the research to be able to properly write up the last major topic that I plan to cover in cat theory. While doing my research on closed cartesian categories and lambda calculus, I came across…
One of the things that we always say is that we can recreate all of mathematics using set theory as a basis. What does that mean? Basically, it means that given some other branch of math, which works with some class of objects O using some set of axioms A, we can define a set-based construction of…
In my last post on the surreals, I introduced how the surreal numbers are constructed. It's really fascinating to look back on it - to see the structure of numbers from 0 to infinity and beyond, and realize that ultimately, that it's all built from nothing but the empty set!
Today, we're going…
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?