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 us for more information.

Servers for rsync are available at rsync.metamath.org and cn.metamath.org. To check availability, use the command "rsync rsync.metamath.org::" or "rsync cn.metamath.org::", which should respond with "metamath metamath". See the mirror.txt file for more information. Note that rsync.metamath.org may be throttled to reduce network load on the development site. If you just want to get a local copy of the site for off-line viewing, the cn.metamath.org rsync server is much faster.

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.
Metamath Music Page - Proofs you can listen to in MIDI format. Fun and edjemacational!: - Haddon Kime (composer, music score for the play Proof)
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"
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"