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
or contact Norman Megill
for more information.
Servers for rsync are available at rsync.metamath.org and
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 is throttled at 1000KB/s 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.
Some comments about this site found on the
web (see HTML source for references)
- 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
- - Haddon Kime (composer,
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
- - John Bethencourt, "Principia
- 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
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"
14-Oct-2019 by N. Megill.
30-Jan-2017 by David A. Wheeler.
comments are welcome: