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 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)
- Metamath. Brain full.
- - Dan Sanderson (BrainLog Archives)
- 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
- - Freek Wiedijk (Mizar Forum)
- Metamath Music Page - Proofs you can listen to in MIDI format. Fun
- - 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
- - John Bethencourt, "Principia
- 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)
- 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
- - 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
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"
This page was last updated on
comments are welcome: