Metamath Site Selection

Please select a mirror site to reach the Metamath Home Page. Note: The preferred mirror for permanent links to specific Metamath pages is us.metamath.org.

Additional mirror sites are always welcome. See the instructions in mirror.txt or contact Norman Megill for more information.

Metamath. Brain full.: - Dan Sanderson (BrainLog Archives)
2+2=4 - ever wondered why?: - Maria Schwartz
A modern Principia Mathematica on the web.: - Josh Purinton
Metamath.org - Giving math its proper treatment.: - Tempus Dictum, Inc.
[GIF Images for Math Symbols] ...not great, but not too bad...: - Prof. William J. Rapaport (U. at Buffalo, SUNY)
What you get when you run mathematics through a disassembler.: - Michael Schaeffer
GIF Images for Math Symbols - Works in ALL Browsers I have tried!: - Ian G. Clark, Ph.D. (University of Newcastle-upon-Tyne)
This site is not for the fainthearted, even among professional logicians.: - AK Dewdney (author, The Turing Omnibus) (review)
Metamath - nice but too basic (and I don't like the way they ignore alpha conversion).: - Freek Wiedijk (Mizar Forum)
Metamath Music Page - Proofs you can listen to in MIDI format. Fun and edjemacational!: - Haddon Kime (composer, music score for the play Proof)
Now a Mizar to Metamath compiler, that would be a very interesting and very useless thing :-): - Freek Wiedijk (Mizar Forum)
Metamath - Exploring proofs of mathematics, quantum logic, and Hilbert Space for fun and, er, whatever.: - Dethe Elza
I've burned a ton of wee morning hours lately poking around in this. Even listened to a bunch of the proofs-as-music... Cool shit.: - Jeff Bone (FoRK Archive)
Say you're a meta-mathematics geek and you really like playing with proofs. Did you know you can make music with proofs? Nerdalicious!: - Cody Clark (crossimpact.net)
Seriously, folks, this site is one of the coolest things I've seen in a long time. If you enjoy formal systems, this site will make you very happy.: - John Bethencourt, "Principia Mathematica Revisited"
Most philosophers agree that contemplation of Reality is the highest form of happiness. So, if you want happiness, play Metamath Solitaire all by yourself.: - Kannan Nambiar (Former Professor and Dean, School of Computer Science, Jawaharlal Nehru University) (review)
Metamath has an archive of mathematical proofs, cross-references, for you to explore. And a very odd section dedicated to translating those proofs into music.: - Matt Webb (interconnected.org)
If set theory (or quantum logic) is more your style, Metamath should be sufficient to keep you for a while, although it can get hard to follow due to lack of prose. (Gotta love the proof that x=x.): - Casey Schneider-Mizell (MetaFilter)
I would consider the Metamath format slightly low-level, with adhoc handling of bound variable scopes; lambda calculus provides a more abstract and clean notion of variable binding and substitution.: - Makarius Wenzel
Wff'n'Proof Rides Again - Ever have that urge to go back and regain the old Wff'n'Proof star? If you grew up with this game you're probably right there with me. Well it may not be the game but the Metamath site sure does take it to new limits.: - Tom Higgins (WSMF Web Thing)
Math is the "universal language" and Metamath is a site dedicated to helping non-mathemeticians learn mathematical proofs. It is not non-complicated (your Euclidean high school geometry class it is not) but it is also well explained and contains the oft-missing inner details.: - "atrox" (screaming-penguin.com)
Care for some mathematical proofs? How about 3000 interconnected proofs in logic and set theory, building from simple axioms. They're all here, hyperlinked up the wazoo. Also available: proof-generation programs, the entire database behind the site, and curiously interesting music generated from the structure of selected proofs.: - Mike Gunderloy (Mike's Weblog)
The Metamath system maybe should not be counted as an "industrial strength" system: it only has one user. However, the system is beautifully executed and differs in many respects from the other systems. For one thing it is very fast: it can check its full (non-trivial) library in only a few seconds. Also it really makes the logical structure of the mathematics completely transparent.: - Freek Wiedijk, "Comparing mathematical provers"
I feel I understand Metamath reasonably well now. It has some issues, but its overwhelming strength is that it's simple. For example, I believe that a fully functional proof verifier could be done in about 300 lines of Python. I wonder how many lines of Python a corresponding verifier for HOL would be; I'd guess around an order of magnitude larger. That kind of difference has profound implications.: - Raph Levien (advogato.org)
...let's look at why mathematical proofs are so difficult to understand for most people...any realistic mathematical proof will leave out a great many steps, which are considered to be the "required background knowledge" for anyone who wants to understand the proof. By the way, a very interesting project called the Metamath project is trying to create an online archive of mathematical proofs which are specified all the way to the bottom, starting from set theory. But this is a very rare exception to the general rule.: - Mike Vanier, "Why I love computer science"