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.
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
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.