Mirror Site SelectionMirror Site Selection Metamath Home Page This page:  FAQ  Downloads  Download help  Reviews
Metamath Proof Explorer - Constructs mathematics from scratch, starting from ZFC set theory axioms. Over 10,000 proofs. Updated 19-Mar-2014.   News and most recent proofs: latest, this mirror
Metamath Proof Explorer
Hilbert Space Explorer - Extends ZFC set theory into Hilbert space, which is the foundation for quantum mechanics. Includes over 1,000 complete formal proofs. Updated 11-Sep-2009.
Hilbert Space Explorer
Quantum Logic Explorer - Starts from the orthomodular lattice properties proved in the Hilbert Space Explorer and takes you into quantum logic with around 1,000 proofs. Updated 28-Oct-2011.
Quantum Logic Explorer
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 16-Feb-2013.
Metamath Solitaire
GIF and PNG Images for Math Symbols - A copyright-free collection of over 1,000 bit-mapped images for math symbols. Updated 30-Nov-2013.
GIF and PNG Images for Math Symbols
Metamath Music Page - Strictly for fun. You can listen to what mathematical proofs "sound" like! Updated 29-May-2006.
Metamath Music Page
21-May-2007    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 in complete detail from first principles, with absolute rigor. Hopefully it will amuse you, amaze you, and possibly enlighten you in its own special way.

Q: Is there a wiki for Metamath?
A: The AsteroidMeta [external] wiki is used for Metamath discussions. There is also a Google Groups [external] mailing list.

Q: Where do I start?
A: Read Sections 1, 2, and 3 of the Metamath Proof Explorer. Then look at a few proofs in Section 4 to make sure you understand how they work.
      You can also experiment with simple proofs in the Metamath Solitaire applet. For a nice independent introduction to logic, see Hirst and Hirst's A Primer for Logic and Proof [external] (PDF, 0.5MB); compare its axioms to ours. Wikipedia has an overview of set theory [external].

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. Some people find this frustrating. 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, even if you don't understand what the symbols mean. 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: Who is the intended audience for Metamath?
A: Metamath is not for everyone, of course. A person with no interest in math may find it boring or, optimistically, might find a spark of inspiration. 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 austere elegance of formal mathematics for its own sake might enjoy just casually browsing through the proofs for their aesthetic appeal.

Q: I already have an abstract mathematics background. 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. With a little practice, this feature, together with the gray indentation levels showing the tree structure, should help you figure out the "important" steps so that you could write down an informal version of the proof if you wanted to.
      (By the way, it's best not to use the colored numbers to reference theorems in an archived discussion, since they change when new theorems are inserted at an earlier point in the database.)

Q: What does the Metamath language look like?
A: The precise technical specification of the language is given in Section 4.1 (p. 92) 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. As an indication of the language's simplicity, Raph Levien independently wrote the remarkably small mmverify proof verifier in Python. 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 has also developed a related 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: What other programs have been written for the Metamath language?
A: The following programs can verify the proofs in a Metamath database file: (1) the original Metamath program (written in C by Norman Megill); (2) mmverify (written in 350 lines of Python by Raph Levien); (3) mmj2 [external] (written in Java by Mel O'Cat, with a GUI proof assistant that optionally interfaces with the Metamath program's CLI proof assistant via the eimm program); (4) Hmm [external] (written in 400 lines of Haskell by Marnix Klooster); (5) verify [external] (written in 380 lines of Lua by Martin Kiselkov; needs 40 min to verify set.mm, but provides an interesting example for learning Lua); (6) Verifer [external] (written in 550 lines of C# by Chris Capel); (7) checkmm.cpp (written in C++ by Eric Schmidt). The following program provides a graphical user interface for displaying the output of the Metamath program commands: (8) mmide [external] (written in Python by William Hale). In addition, the following programs verify proofs in their own languages derived from Metamath: (9) gh_verify [external] (for the Ghilbert language; written in Python by Raph Levien); (10) Shullivan [external] (also for the Ghilbert language; written in C by Dan Krejsa; loads and verifies the translated set.mm in 500 ms); (11) Bourbaki [external] (for a custom Lisp-like language; written in Common Lisp by Juha Arpiainen); (12) JHilbert [external] (written in Java by Alexander Klauer), a proof verifier for collaborative theorem proving "in the spirit of Ghilbert" and the engine behind Wikiproofs [external]; and (13) Russell [external] (written in C++ by D. Yu Vlasov), built upon Metamath as a high level superstructure with an automatic proving facility, described in a paper [external] (in Russian) and reviewed here.

Q: Why is it called "Metamath"?
A: It means "metavariable math." See A Note on the Axioms. Metamath shouldn't be confused with metamathematics (occasionally abbreviated metamath, metamaths, or meta math), which is a specialized branch of mathematics that studies mathematics itself, leading to results such as Gödel's incompleteness theorem. An expert in the latter is called a metamathematician, so to avoid confusion one might use "metamathician" for someone knowledgeable about Metamath.

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. Four well-known projects are Prover9 [external], HOL [external], Isabelle [external], and Coq [external]. Freek Wiedijk wrote an interesting collection of notes [external] comparing several mathematical proof languages. His book, The Seventeen Provers of the World [external] (PDF, 0.6MB), compares the proofs that the square root of 2 is irrational in 17 proof languages, including Metamath (theorem sqr2irr).
     Unlike most other systems, Metamath attempts to use the minimum possible framework needed to express mathematics and its proofs. Other systems do not consider that aspect necessarily important, and their underlying computer programs can be large and complex in order to perform mathematical reasoning at a higher level. Metamath's proofs are often quite long compared to those of other systems, but they are completely transparent with nothing hidden from the user. All reasoning is done directly in the proof itself rather than by algorithms embedded in the verification program. Metamath is unique in this sense, offering an alternative approach for those attracted to its philosophy of simplicity.


Downloads
  • metamath.pdf (1.3 MB)
    • Description: The Metamath book (211 pp.), which provides an in-depth understanding of the Metamath language and 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. The LaTeX source file for the book is metamath.tex (0.6 MB; the comment at the beginning explains how to compile it). A paperback version [external] of the Metamath book (ISBN 978-1-4116-3724-5) is also available if you prefer a printed copy.

      BibTeX citation:

      @Book{metamath,
        author =       {Norman D. Megill},
        title =        {Metamath: A Computer Language for Pure Mathematics},
        year =         {2007},
        publisher =    {Lulu Publishing},
        address =      {Morrisville, North Carolina},
        note =         {{\tt http://us.metamath.org/downloads/metamath.pdf}},
      }
      
       New 4-Jul-2011 John D. Baker has kindly provided (metamath_kindle.zip) "a modified version of [the] metamath.tex book source that is formatted for the Kindle. If you compile the document the resulting PDF can be loaded into into a Kindle and easily read." The compiled PDF file is also included.
  • metamath.tar.bz2 (4.3 MB) or metamath.tar.gz (5.2 MB) or metamath.zip (5.3 MB)
    • Description: The Metamath program (version 0.106 30-Mar-2014), which is an ASCII-based 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 *.mm ASCII databases (set.mm and others) are also included in this download.
    • Instructions: 1. Extract all files, which will be contained in a directory called "metamath". 2. For Windows, double-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 (above) for an in-depth understanding.
    • To uninstall: Just delete the "metamath" directory. Nothing else on your system was touched by the installation.
    • Notes:
      • Quicker installation for Windows users who just want the main (set.mm) database: 1. Download the Metamath program metamath.exe (0.5MB) 2. Download the set.mm database (16MB) into the same folder. 3. Double-click on "metamath.exe" and type "read set.mm". 4. To uninstall, just delete these two files. Nothing else is touched on your system.
      • On MacOSX, select the Terminal application from Applications/Utilities to get to the command line. On recent versions of MacOSX, you need to install gcc separately. Typing "whereis gcc" will return "/usr/bin/gcc" if it is installed. The XCode package is typically used to install it, but it can also be installed without XCode[external].
      • On Linux/MacOSX/Unix, the Metamath program will be more pleasant to use if you run it inside of rlwrap [external], which provides up-arrow command history and other command-line editing features. After you install rlwrap per its instructions, invoke the Metamath program with "rlwrap ./metamath set.mm". (Thanks to Marnix Klooster for bringing rlwrap to my attention. The Windows version of the Metamath program, by the way, was compiled with lcc, which has some similar features built-in.)
  • mmj2.zip (4.4 MB) (latest official version, 9-Jan-2014)
    mmj2-orig.zip (Mel O'Cat's last official version, 11-Oct-2011)
    TESTmmj2jar.zip (Mel O'Cat's last test version, 20-Sep-2012, with search and GUI enhancements)
    https://github.com/digama0/mmj2 (development repository)
    • Description: Mel O'Cat's mmj2 GUI Proof Assistant for the Metamath language. Includes thorough file validation and proof verification, syntactic parsing of Metamath formulas and many other features.
    • Instructions: Download mmj2jar.zip, unzip and read the enclosed documentation. Help/Assistance provided at the Asteroid Meta wiki mmj2 page [external].
    • Quick startup for Windows:
      • 1. Download mmj2.zip and unzip it (wherever)
      • 2. Copy the mmj2\mmj2jar directory to C:
      • 3. Edit C:\mmj2jar\RunParms.txt (with e.g. Notepad).   Locate the line "LoadFile,c:\metamath\set.mm" and change it to point to your set.mm file
      • 4. Start -> All Programs -> Accessories -> Command Prompt
      • 5. Type:
             CD C:\mmj2jar
             mmj2.bat
    • Notes:
      • The eimm export-import program links the mmj2 and Metamath proof assistants without exiting from either program, giving you the features of both during proof development.
      • The mmj2 directory listing also has the source code, older releases, and MD5 checksums.
  • mpegif.tar.bz2 (50 MB) or mpegif.tar.gz (100 MB) or mpegif.zip (130 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 22,000) into a directory called "mpegif". The home page is the file "mmset.html". You will need about 1.5 GB of free space.
  • qlegif.tar.bz2 (1 MB) or qlegif.tar.gz (2.5 MB) or qlegif.zip (4 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.3 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.3 MB) or symbols.zip (0.8 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".
  • mmverify.py (version of 27-Jan-2013)   (previous version)
    • Description: Raph Levien's independently-written Python proof verifier for the Metamath language.
    • Instructions: See the comments at the top of the program listing.
  • eimm.zip (0.03 MB)   New 18-Apr-2006
    • Description: An experimental proof export-import program (version 0.07 18-Oct-10) that translates incomplete proofs in progress between the Metamath program's CLI Proof Assistant and Mel O'Cat's mmj2 GUI Proof Assistant, without exiting from either proof assistant, giving you the features of both assistants during proof development.
    • Instructions: Extract all files into a directory called "eimm". See the readme.txt file for detailed instructions. A pre-compiled Windows binary is provided; gcc is required to compile for Linux/MacOSX/Unix.

        Metamath program's Proof Assistant (MM-PA> prompt)
                        |            ^
                        |            |
          submit eimmexp.cmd /s   submit eimmimp.cmd /s
                        |            |
                        v            |
                 [*.mmp proof worksheet file]
                        |            ^
                        |            |
                    File/Open    File/Save
                        |            |
                        v            |
                   mmj2 GUI Proof Assistant

    • Status: There are no known bugs. The development of this prototype is believed to be complete. The only change in the future might be to incorporate the import-export algorithms natively as Metamath program commands, for convenience. Suggestions for other possible features are, of course, welcome.
  • 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 a C compiler such as gcc.
    • Note:
      • The above programs are frozen at the versions used for the papers and will reproduce the papers' results exactly. The most recent versions of these programs and others (in particular states.c and latticego.c, described in a paper in progress) 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 (100 MB) or metamathsite.tar.gz (110 MB) or metamathsite.zip (120 MB)
    • Description: A mirror of the entire Metamath web site including all the downloads listed above (that aren't external links). 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 3.5 GB of disk space will be used.
    • Instructions: Extract all files into a directory called "metamathsite". Go to that directory then type "./install.sh". This may take several hours 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:
      • See the README.TXT file that accompanies the download for more detailed instructions.
      • Another way to install your local copy is with rsync (on Linux/MacOSX/Unix or Cygwin). The download will be compressed to about 2GB and automatically expanded to about 3.5GB. 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. Note that you need twice the disk space during rsync, i.e. 7GB.
      • A third way to install your local copy is with wget (see the Download and Extraction Help below). The full uncompressed 3.5GB 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 mirror.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 Programs -> Accessories -> Command Prompt. If Command Prompt is missing, then from the Start menu, choose Run..., type CMD (or COMMAND 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 have been told that 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 has been recommended for Windows is ToX [external]. (For Linux/MacOSX/Unix, use the command: sed -e 's/$/\r/' unixfile > windowsfile. To go back, use the command: tr -d '\015' < windowsfile > unixfile.)

On Windows, the "write source" command in the Metamath program will automatically convert .mm database text files from Unix format to Windows format (and vice-versa on Linux/MacOSX/Unix).


Note: Some of the links in the section below are obsolete. Let me know if you have current links. --NM 16-Feb-2013
Reviews
The Assayer logo

The Assayer open-content book reviews (Jan. 8, 2004)

U Waterloo logo

University of Waterloo
Archimedes' Sandbox Reviews (Oct. 28, 2002)

MERLOT logo

Multimedia Education Resource for Learning and Online Teaching (Jul. 21, 1997)

Also: John Bethencourt, Principia Mathematica Revisited (Jan. 24, 2004)
Also: American Scientist, Metamath (site of the week) review (Jul. 25, 2005) [link broken, 28-Feb-2009]
Also: University at Albany Science Library, 2007 Top 30 Science Resources (Dec. 20, 2007)
Directories
Wikipedia logo

Wikipedia

Math Forum logo

Drexel University's Math Forum Internet Mathematics Library (another mention)

Education Portal logo

Government of Australia Education Portal

Britannica logo

Encyclopædia Britannica "approved iGuide site" (Oct. 11, 2006) (free set theory full text article)

Awards
Golden House Sparrow Award

The Golden House Sparrow Award: Site of the Day (Jul. 20, 2000) (check out their eclectic current page)

Scout Report for Science and Engineering

Scout Report for Science and Engineering Selection (Jul. 19, 2000)

Knot a Braid of Links logo

Knot a Braid of Links "Cool math site of the week" (Jul. 7-13, 1998)

Rated Top 25% WebApplet by JARS

Rated by JARS (Apr. 26, 1998)


This page was last updated on 30-Mar-2014.
(Hidden files) symbols
Your comments are welcome: email Norman Megill               Donations and volunteering
Copyright terms for this page: Public domain except the images below "Reviews"
Valid HTML 4.01!