The Metamath Home Page

metamath.planetmirror.com/

Metamath is a language developed by Norman Megill, an M.I.T. alumnus with enormous energy and a commitment to metamathematics, set theory, logic and quantum mechanics. This site is not for the fainthearted, even among professional logicians.

The language is succinct but has made possible much cleaner and more consistent proofs. There is even a proof-checker that separates real proofs from those containing errors, however subtle. Megill’s passion has led him into many mysterious corners of his subject, including a way to convert (meta)mathematical proofs into music!

What You See

Well, almost nothing. Below the title the only welcome note is sounded by a brief warning to bookmark the site as in case content changes at this particular URL. Below the warning note there are six other pages to visit, as well as four download options for various books , software, or databases. The six main features of this site are: The Metamath Proof Explorer; The Metamath Music Page; The Hilbert Space Explorer; The Quantum Logic Explorer; Metamath Solitaire; and Classic Metamath. As well, visitors to this site may download the Metamath Book, the Metamath Proof Explorer Database; the Quantum Logic Explorer Database, and the source code for Metamath Solitaire.

The Metamath Proof Explorer is relatively massive, consisting of 60 megabytes of web pages with over 3000 detailed proofs and deductions in logic and set theory. “Each proof,” says the author, “is pieced together with razor-sharp precision using simple rules...” And “Armchair mathematicians can spend literally days exploring the complex tangle of logic leading, say, from 2 + 2 = 4 back to the axioms of set theory.” If that isn’t fun, what is? The Metamath Music Page offers some eerie sounds that will certainly pass for music in avant-garde circles. We must admit to a certain fascination at hearing the steps of a proof rendered as notes that occasionally announce themes, only to abandon them. The Hilbert Space Explorer opens a window on Hilbert space, the scene of virtually all quantum mechanical action. It proceeds grandly from axioms and definitions through basic theorems to the properties of orthomodular lattices and quantum mechanics. The Quantum Logic Explorer promises a “wild” trip into quantum logic, a mathematic that is not even known to be decidable (or not). Here are over 800 proofs by the author and a few colleagues. We are happy to learn that all the proofs have been checked by the Metamath proof checker but the author surely sugar-coats things when he claims it to be “the most ornery, intractable logic you will probably ever encounter.” In Metamath Solitaire visitors can build their own proofs in logic and set theory. Classic Metamath is “for the serious user.” It leads off into grey pages with detailed explanations of how to access the formal proofs of over 2000 theorems.