[Image of
aleph-naught] Metamath Site Selection Quick links to:
Theorem list
Most recent proofs

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 us.metamath.org   Primary mirror (United States). Web server statistics.
AT at.metamath.org   Secondary mirror (Austria) [courtesy of LIGE IT-Solutions]
CN cn.metamath.org   Terciary mirror (China) [courtesy of caiyunapp.com]
DE de.metamath.org   Quaternary mirror (Germany)
KR kr.metamath.org   Quinary mirror (S. Korea) [courtesy of 0xf.kr]
US us2.metamath.org:88   Development site (United States) (Some users have reported blocking of nonstandard ports. You can also use us2.metamath.org:443 or us2.metamath.org:8888.)

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.

Some comments about this site found on the web (see HTML source for references)
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"


Valid HTML 4.01!
Updated on 26-Sep-2017 by N. Megill.
Updated on 30-Jan-2017 by David A. Wheeler.
Your comments are welcome: Norman Megill nm at alum dot mit dot edu