Q: What is Metamath?
A: Metamath is a tiny language that can express theorems in abstract mathematics, accompanied by proofs that can be verified by a computer program. This site has a collection of web pages generated from those proofs and lets you see mathematics developed formally from first principles with absolute rigor. Hopefully it will amuse you, amaze you, and possibly enlighten you in its own special way.
It has certainly amused and amazed me. (Note: If you don't consider the Zermelo-Fraenkel axioms “one of the most profound achievements of mankind” [here], Metamath might not be for you.)
Metamath is a database of machine-verifiable mathematical proofs. This is actually something of a long-term dream of mine, so I'm surprised and impressed.
Here are the frustrating bits:
The database is largeish, but its reach is very limited. Metamath currently comprises 6,403 theorems, of which “2+2=4” is number 5,214.
The proofs themselves are unenlightening. For example, Metamath has proved that there are infinitely many primes. But click the link. It's totally indecipherable.
What I'd do differently, to try and address those problems:
Make the database more searchable, by giving pages readable English names, not numbers or junk like
caoprmo.Allow anyone to edit.
Encourage more English text mixed in with the formal statements.
Allow pages with non-verifiable proofs, missing steps, syntax errors, etc. But if a proof is correct and verifiable, you'd get a nice string of green lights down one side of the page.
Work hard on notation. It has to be human-editable and human-readable. (This strikes me as extremely difficult.)
I wouldn't require contributors to prove every step formally. This requires a deep understanding of formal logic that most mathematicians frankly don't have. Instead, you'd just type all the steps in the proof, with the usual gaping logical chasms in between; and the system would use automatic theorem provers to check that each step follows from the preceding ones. This would help with both readability and reach.
Now theorem provers suck, so often the system won't be able to prove every step. No problem. Contributors could close a gap by (a) giving the system a hint (e.g. adding the words “...by [[Schphlebotsky's Theorem]]”), (b) inserting a clarifying intermediate step, or (c) making a separate page proving the step as a lemma. And they could work incrementally.
Metamath is already more and better than I would've thought possible. And there are extremely good reasons that Metamath exists and my idea is just a dream. But I think the dream has potential. Who knows—Metamath might evolve in this direction.
2 comments:
A commenter over at Scott Aaronson's place has linked here. Scott was replying to a comment from Bram Cohen about automated theorem checking. Bram views "the switch to doing mathematics in the style just described [i.e. making proofs machine-checkable] as inevitable..."
I like your ideas about incremental proof development - that seems like exactly the right way to go. Roughly, whenever someone enters a putative proof A=>B=>C...=>Z, each of the steps should be checked (and if necessary and possible, filled out into a verifiably valid deduction), and then any uncompleted steps are subbed off as unproven Lemmas. There'd presumably be a page of links to "Lemmas needing attention", sort of like Wikipedia's Wanted Pages list.
You've talked about Metamath, but do you have any preference for this over other automated systems like HOL or Mizar? (Sorry if you've written about this loads already - I've just got here and haven't read through your previous posts yet).
My main concern for the health of such a project is that standardization on some particular language (like Metamath, or HOL) may turn away people who don't like that style. Each of those projects has a community of users who spend their spare time transcribing proofs into that language, but who evidently don't trouble to do the same for other languages (since the different projects have made different amounts of progress).
You might avoid this problem if you had proofs coded in a language that's so nice that essentially everyone likes it - like the LaTeX of proofs. But better yet would be the ability to translate from one language to another. Then any proof can be written in the writer's preferred language, and displayed in the reader's favourite. It would also mean that the existing databases of proofs in those various projects could be rolled together to give a good starting point.
I've just been watching the lecture on Generic Operators in the SICP series, so separating the representation (in the machine) from the presentation (to the user) seems the natural thing to do. Ideally, someone would eventually write something that turned formal proofs in the system into readable papers. And someone else would write an interface that output proofs formatted in Leslie Lamport's nested style, and so on.
You've talked about Metamath, but do you have any preference for this over other automated systems like HOL or Mizar?
No. I don't know enough to have an informed opinion.
I am not sure what to do about multiple languages and styles. I am not as confident as you are about translation. I think different systems will have incompatible beliefs. If one system uses a Dedekind construction of the reals and maybe another uses a different construction, neither will be able to reason about Theorempedia's reals, which I imagine will be defined axiomatically (and the various constructions will be theorems). But let's suppose this problem can be solved.
I have changed my mind about one thing. I think probably Theorempedia doesn't need provers of its own; instead, it can use distributed brainpower. If you have written a hot-shot prover, then you can easily write a spider that constantly walks Theorempedia, pulls out unproven steps, and poses them to the prover as problems. When your prover proves a step, it submits the proof in a form Theorempedia can check. Any number of provers could do this. It could get pretty competitive, if we're lucky...
From the ordinary mathematician's point of view, he just enters a high-level proof, which Theorempedia per se isn't smart enough to check. He comes back the next day, and all the lights are green. Overnight, a theorem-prover in Germany was able to prove most of his steps, and one in Singapore proved the others. Sounds pretty good to me.
All Theorempedia needs is a common rock-bottom proof-checking algorithm--the base case. Then with minimal cleverness it can check new low-level submissions. Ultimately you should be able to query Theorempedia for a machine-readable proof that contains all the steps, which you may then check yourself in O(N) time. Metamath just happens to be the project I've seen that puts the most emphasis on how simple this is.
Post a Comment