|
Hilbert Space Explorer -
Extends ZFC set theory into Hilbert space,
which is the foundation for quantum mechanics. Includes around
700 complete formal proofs. Updated 14-Dec-2004.
|
|
|
|
Quantum Logic Explorer -
Starts from the orthomodular lattice properties proved in the
Hilbert Space Explorer and takes you into
quantum logic with around 900 proofs.
Updated 4-Dec-2004.
|
|
|
|
Metamath Solitaire - A Java
applet
that demonstrates simple proofs. Built-in axiom systems
include ZFC; modal, intuitionistic, and quantum logics; and Tarski's
plane geometry.
Updated 4-Dec-2004.
|
|
|
Metamath Music Page - Strictly for fun.
You can listen
 0:16
to what mathematical proofs "sound" like!
Updated 31-Dec-2004.
|
|
|
5-Aug-03 Some
advanced and difficult miscellaneous open
problems related to Metamath and other topics on this site.
Mini FAQ
Q: What is Metamath?
A: Metamath is a tiny language that
can express theorems in abstract mathematics, accompanied by proofs that
can be verified by a computer program. This site has a collection of
web pages generated from those proofs and lets you see mathematics
developed formally from first principles with absolute rigor. Hopefully
it will amuse you, amaze you, and possibly enlighten you in its own
special way.
Q: Will Metamath help me learn abstract
mathematics?
A:
In order to follow a proof in an advanced math textbook, you may need to
know prerequisites that could take years to learn. This frustrates a
lot of people. In contrast, Metamath uses a single, simple substitution
rule that allows you to follow any proof mechanically. You can
actually jump in anywhere and be convinced that the symbol string you
see in a proof step is a consequence of the symbol strings in the
earlier steps that it references. But this is quite different from
understanding the meaning of the math that results. Metamath
alone probably will not give you an intuitive feel for abstract math, in
the same way it can be hard to grasp a large computer program just by
reading its source code, even though you may understand each individual
instruction. However, the Bibliographic
Cross-Reference lets you compare informal proofs in math textbooks
and see all the implicit missing details "left to the reader."
Q: Where do I
start?
A: To gain a rough feel for what some of the symbols mean, as
well as a general overview, you can browse the Wikipedia*
pages describing
propositional
calculus [external], predicate
calculus [external], and set theory
[external].
In the Metamath Proof Explorer learn how proofs work, read
about the axioms, then browse through
some proofs in propositional
calculus. You can also
experiment with simple proofs in the Metamath Solitaire applet.
If you are serious about learning logic and set theory, you
shouldn't depend on this site alone but should study it in conjunction
with one or more standard textbooks.
Two on-line books are
Hirst and Hirst's A
Primer for Logic and Proof [external] (PDF, 0.5MB)
and
Stefan Bilaniuk's A Problem
Course in Mathematical Logic [external] (PDF, 0.7MB).
* Some math symbols on the
Wikipedia pages do not render in Internet Explorer 6.0. You can use Firefox or Mozilla [external] if you want
to see them. (Firefox and Mozilla will also correctly display the
faster-loading Unicode version of our Metamath Proof Explorer
pages.)
Q: Who is the intended audience for
Metamath?
A: Metamath is not for everyone of course. A person with little
interest in abstract math may find it, well, uninteresting.
Professional mathematicians may view it as a curiosity more than a tool
- they need to do things at a high level to work efficiently. On the
other hand Metamath can appeal to those who enjoy picking things
apart to see how they work. Others may
like the absolute rigor that Metamath
offers.
Someone new to logic and set theory, who
is still developing the mathematical maturity needed to follow informal
textbook proofs, may find some reassurance in Metamath's
step-by-step breakdown.
And anyone who
appreciates the stark beauty of mathematics for its own sake might enjoy
just casually browsing through the proofs for their aesthetic appeal.
Q: I'm a
mathematician (or advanced student). How can I grasp the key
ideas in a Metamath proof more quickly?
A: On the web page with the proof, look at the little colored numbers in the Ref column. The steps with the largest
numbers are usually the ones you want to look at first. The steps with
smaller numbers are typically logic "glue" to tie them together. The
colors follow roughly the rainbow colors as the statement number
increases, so that the largest numbers tend to stand out from the
others. This feature, combined with the gray indentation levels showing
the tree structure, should help you figure out a higher-level outline of
the proof more efficiently.
Q: What does the
Metamath language look like?
A: The precise technical specification of the language is given
in Section 4.1 (p. 88) of the Metamath book
and is about 4 pages long. A simple example is given on p. 35.
Compare this source screenshot with
the generated web page. But you
don't have to know or even look at the language if you just want
to follow the proofs on these web pages.
The Metamath program is the main tool for working with
the Metamath language. In addition, an independent and remarkably small
proof verifier was written in Python by
Raph Levien. He writes, "I find the whole thing a bit magical. Those
300 lines of code, plus a couple dozen axioms, effectively give you the
building blocks for all of mathematics." (Raph is also developing a new
language called Ghilbert
 external]
that improves upon Metamath by guaranteeing the soundness of
definitions and providing features useful for collaborative work.)
Bob Solovay wrote a nicely commented
presentation of Peano arithmetic in the Metamath language, peano.mm, that is worth reading as a
stand-alone file.
Q: Why is it called
"Metamath"?
A: This is explained in A
Note on the Axioms, in the fifth paragraph.
Q: The symbol " " shows up
in some set theory proofs such as this
one. What does it mean?
A: See the Deduction Theorem.
Q: Are there other sites that formalize math
from its foundations?
A: Another project that aims to rigorously formalize and verify
math is Mizar [external]. It is intended to
appeal to professional mathematicians and requires a certain
mathematical maturity to be able to follow its proofs. It tries to
mimic mathematical proofs they way they are normally published, whereas
Metamath shows you every little detail.
Beyond verification is the field of
automated theorem proving. Two well-known projects are Otter [external] and Isabelle
[external].
Freek Wiedijk wrote an interesting collection of notes [external]
comparing
several mathematical proof languages.
Downloads
-
mpegif.tar.bz2 (4 MB) or
mpegif.tar.gz (11 MB) or
mpegif.zip (20 MB)
- Description: The complete set of
Metamath Proof Explorer web pages.
Includes the Hilbert Space Explorer and the Metamath Music Page. (Does
not include the Unicode font version of the pages.)
- Instructions: Extract all files
(around 5,600) into a directory
called "mpegif". The home page is the file "mmset.html". You will need
about 230 MB of free space.
-
qlegif.tar.bz2 (0.6 MB) or
qlegif.tar.gz (1.6 MB) or
qlegif.zip (3.1 MB)
- Description: The complete
set of Quantum Logic Explorer web pages.
- Instructions: Extract all
files (around 1,000) into a directory
called "qlegif". The home page is the file "mmql.html".
-
mmsolitaire.tar.bz2 (0.2 MB) or
mmsolitaire.tar.gz (0.2 MB) or
mmsolitaire.zip (0.2 MB)
- Description: The Metamath
Solitaire web page, compiled Java applet,
and applet source code.
- Instructions: Extract all files
into a directory
called "mmsolitaire". Use the page "mms.html" to run the applet.
-
symbols.tar.bz2 (0.2 MB) or
symbols.tar.gz (0.2 MB) or
symbols.zip (0.6 MB)
- Description: A collection of
over 1,000 mathematical symbols
in the form of transparent GIFs that you can use on your own web pages.
- Instructions: Extract all
files into a directory
called "symbols". The home page is the file "symbols.html".
-
metamath.tar.bz2 (1.3 MB) or
metamath.tar.gz (1.6 MB) or
metamath.zip (1.6 MB)
- Description: The
Metamath program, which is an ANSI C
program with a command-line interface. It was used to build and
verify the proofs in the Metamath Proof Explorer, as well as to generate
its web pages. The ASCII databases (*.mm files) are also included.
- Instructions: 1.
Extract all files
into a directory called "metamath". 2. For Windows, click on
"metamath.exe" and type "read set.mm". For Linux/MacOSX/Unix,
compile with the command "gcc *.c -o metamath" inside the
"metamath" directory, then type "./metamath set.mm" to run.
3. For
all systems, once in the program, use the "help" command to guide you.
Consult the Metamath book (below) for an in-depth understanding.
(The web pages on this site were generated with
"show statement * /html".)
- To uninstall: Just delete the
"metamath" directory. Nothing else on your system was touched by the
installation.
- metamath.pdf
(1.3 MB)
- Description: The
Metamath book (176 pp.), which
provides an in-depth understanding of the Metamath program. The first
part of the book also includes an easy-to-read informal discussion of
abstract mathematics and computers, with references to other proof
verifiers and automated theorem provers. [This PDF file was generated from the
LaTeX source file metamath.tex (0.6 MB).]
- mmverify.py (0.01 MB)
- Description: Raph Levien's
independently-written Python
proof verifier for the Metamath language.
- finiteaxiom.pdf (0.2 MB)
- Description: Preprint of the
article "A Finitely
Axiomatized Formalization of Predicate Calculus with Equality," which
provides the theoretical basis for Metamath and is referenced on the
Metamath Proof Explorer pages. [This PDF file was generated from the LaTeX
source file finiteaxiom.tex (0.1 MB).]
- weakd.pdf (0.2 MB)
- Description: The article
"Weaker D-Complete Logics," which
is referenced in the Metamath Solitaire applet.
- Quantum logic papers
- Description: Several papers
on quantum logic,
orthomodular lattices, and Hilbert space
can be downloaded from here.
-
quantum-logic.tar.bz2 (0.05 MB) or
quantum-logic.tar.gz (0.1 MB) or
quantum-logic.zip (0.1 MB)
- Description: Several
programs (lattice.c, latticeg.c,
beran.c, bercomb.c)
referenced in the papers "Algorithms for Greechie Diagrams" and
"Orthomodular Lattices and a Quantum Algebra."
- Instructions: Extract all
files into a directory called "quantum-logic". See the README.TXT
file therein for instructions on compiling and using the programs.
You will need an ANSI C compiler such as gcc.
- Note: The most recent versions
of these programs, and others, are available at ftp://users.shore.net/members/n/d/ndm/quantum-logic/ [external].
Each .c file is a stand-alone program. After compiling (under
Linux/Cygwin/MacOSX/Unix) with "gcc program.c -o program",
type "./program --help" for instructions.
-
metamathsite.tar.bz2 (2.9 MB) or
metamathsite.tar.gz (3.5 MB) or
metamathsite.zip (4 MB)
- Description:
A mirror of the entire Metamath web site
including all the
downloads listed above. This can be useful if you have a slow phone
line connection or want to browse the site off-line. A script builds
the site from source files and requires a Linux/MacOSX/Unix operating
system (or the free Cygwin [external]
for Windows).
About 550MB of disk space will be used (or burn it to a CDROM).
- Instructions:
Extract all files into a directory called "metamathsite". Go to that
directory then type "./install.sh". This
may take an hour or more to run. The home page (this page) will be
"index.html".
- In Cygwin, to go to a directory, type
"cd c:/tmp/metamathsite" if your directory (folder) is
C:\tmp\metamathsite.
- On MacOSX, select
the Terminal application from
Applications/Utilities to get to the command line.
- To uninstall: Just delete the "metamathsite" directory.
Nothing else on your system was touched by the installation.
- Notes:
- The script install.sh is the actual script used to periodically
rebuild this site. In the unlikely event there is a problem, see the
notes in install.sh (and please report it to me). During the
installation, a lot of status messages will flash by on the screen,
ending with a final success message if there were no
errors.
- Another way to install your local copy is with rsync (on
Linux/MacOSX/Unix or Cygwin). The download will be compressed to about
80MB and automatically expanded to about 550MB. Create and go to the
metamathsite directory, then type (including the last period):
rsync -vrltS -z --delete --delete-after
rsync://rsync.metamath.org/metamath .
Rerunning this same command
periodically will also keep your copy updated, downloading only the
files that changed. - A third way to install your local copy is with wget (see the Download and Extraction Help below). The full
uncompressed 550MB site will be downloaded, so it will take a long time,
depending on your connection speed. Create and go to the metamathsite
directory, then type:
wget -nH --mirror
"http://us.metamath.org/index.html"
- If you would like to set up a mirror site for public access, read
the instructions in README.TXT.
Download and Extraction Help
Downloading Some browsers may
have problems downloading large binary files. The free wget [external]
program downloads correctly and is available for all platforms including
Windows. Here are the instructions for Windows: - Go to ftp://sunsite.dk/projects/wget/windows/
[external] (or another mirror site) and download wget-1.8.2b.zip
(272kB).
- Extract the file called WGET.EXE
into the folder you will be using for your downloads. The other files
are not needed for a minimal installation.
- From the Start menu, choose Run..., type
COMMAND (or CMD in Windows 95/98), and click OK.
- In the DOS or command window, type
drive-letter:
and press Enter, where drive-letter (C,
D, E,...) is the disk you will be using for your downloads. Then
type
cd folder
and press
Enter, where folder is the folder (without the drive letter and
colon) you will be using for your downloads. - Type
wget "url"
(include the quotes around url) and press Enter, where
url is the URL (internet address, which begins with "http://" or
"ftp://") of the .tar.bz2 or other file you want to download. Most
browsers can copy a URL from a web page display, for example by
right-clicking on the link and selecting "Copy Shortcut" or "Copy Link
Location", which you can then paste into the wget
argument. To paste, right-click on the top of the command window
and select Edit -> Paste. - If you have trouble retrieving FTP files because you are behind
a network firewall, try typing
wget
--passive-ftp "url"
Extracting To
extract .tar.bz2 files in Linux/MacOSX/Unix, use the command "tar
-xjf xxx.tar.bz2", where xxx corresponds to the file name.
To preview what will be extracted, use the command "tar -tjf
xxx.tar.bz2 | more"; press the space bar to show the next page
and "q" to quit the preview. (On MacOSX, select the Terminal
application from Applications/Utilities to get to the command
line.)To extract .tar.gz files in Linux/MacOSX/Unix, use "tar -xzf
xxx.tar.gz". To preview them, use "tar -tzf xxx.tar.gz |
more". To extract .zip files in Linux/MacOSX/Unix, use "unzip
xxx.zip". To preview them, use "unzip -l xxx.zip |
more". To extract .tar.gz and .zip files in Windows, you can use
WinZip, WinAce, or WinRAR, among others. Of these, I think only WinRAR
can extract .tar.bz2 files. Recent Windows versions will open .zip
files automatically. If you have the free Cygwin [external] installed, you can use
the Unix commands above for .tar.bz2, .tar.gz, and .zip files.
Text files The
ASCII (text) files in the downloads are in Unix
format, which uses a bare line-feed character at the end of each line.
This may cause them to display improperly in some Windows text editors
such as Notepad, which requires a carriage-return/line-feed combination.
The better text editors don't have this problem, but if you need to
convert the format, a free program that will do the job is
ToX
[external].
| Reviews |
 MathForge (Jan. 23, 2004) |
 The Assayer open-content book
reviews (Jan. 8, 2004) |
 University of Waterloo
Archimedes' Sandbox Reviews (Oct. 28, 2002) |
 Multimedia Education Resource for
Learning and Online Teaching (Jul. 21, 1997) |
|
Also: John Bethencourt,
Principia
Mathematica Revisited (Jan. 24, 2004)
|
|
|---|
| Directories |
 Drexel University's Math Forum Internet
Mathematics Library |
 dmoz Open Directory Project |
 Library and Information
Services
University of Wales Swansea |
 The Internet Guide to Engineering,
Mathematics, and Computing |
|
|---|
| Awards |
 The Golden House Sparrow Award:
Site of the Day (Jul. 20, 2000) |
 Scout
Report for Science and Engineering Selection (Jul. 19, 2000) |
 Knot a Braid
of Links "Cool
math site of the week" (Jul. 7-13, 1998) |
 Rated by JARS (Apr. 26, 1998) |
|
Mirror Site
Selection
