Metamath Site Selection Quick links to:Theorem listMost recent proofs Google Group Developers

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

 us.metamath.org   Primary mirror (United States)
 at.metamath.org   Secondary mirror (Austria) [courtesy of LIGE IT-Solutions]
 cn.metamath.org   Secondary mirror (China) [courtesy of caiyunapp.com]
 us2.metamath.org   Development site (United States)

Additional mirror sites are always welcome. See the instructions in mirror.txt or contact Norman Megill 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.