Q: How can I askquestions or discuss Metamath-related topics?
A: The MetamathGoogle Group [retrieved 22-Sep-2020] mailing list is being used fordiscussion about Metamath. If you have questions, that is a good placeto ask them. (The AsteroidMeta [retrieved 22-Sep-2020] wiki was used for many olderMetamath discussions, but is no longer available. Archived discussionssuch as this one can be found on archive.org.)

Q: Where do Istart?
A: Read Sections 1, 2, and 3 of the Metamath Proof Explorer. Then look at afew proofs in Section 4 to makesure you understand how they work.
Knowledge of mathematicscan be helpful, although it isn't strictly necessary to be able tomechanically follow the proofs on this site. If you want to startacquiring a higher-level understanding, anice independent introduction to logic is Hirst andHirst's A Primerfor Logic and Proof [retrieved 27-Sep-2017] (PDF, 0.5MB); compare its axioms to ours.Wikipedia has an overview of set theory[retrieved 4-Aug-2016].The video series"Introduction to Higher Mathematics" by Bill Shillito[retrieved 27-Sep-2017] may also be helpful.
You can experiment with simpleproofs in the Metamath Solitaireapplet.To actually create real metamath proofs, you'll want todownload a tool.A common tool is mmj2.David A. Wheeler produced an introductory video, "Introduction toMetamath mmj2" [retrieved 4-Aug-2016].

Q: Will Metamathhelp me learn abstract mathematics?
A:Yes, but probably not by itself.In order to follow a proof in an advanced math textbook, you may need toknow prerequisites that could take years to learn. Some people findthis frustrating. In contrast, Metamath uses a single, simple substitution rule that allows you tofollow any proof mechanically. You can actually jump in anywhereand be convinced that the symbol string you see in a proof step is aconsequence of the symbol strings in the earlier steps that itreferences, even if you don't understand what the symbols mean. Butthis is quite different from understanding the meaning of themath that results. Metamath alone probably will not give you anintuitive feel for abstract math, in the same way it can be hard tograsp a large computer program just by reading its source code, eventhough you may understand each individual instruction. However, the Bibliographic Cross-Reference lets youcompare informal proofs in math textbooks and see all the implicitmissing details "left to the reader."

Q: Who is theintended audience for Metamath?
A: Metamath is not for everyone, of course. A person with nointerest in math may find it boring or, optimistically, might find aspark of inspiration. Professional mathematicians may view it as acuriosity more than a tool - they need to do things at a high level towork efficiently. On the other hand, Metamath can appeal to those whoenjoy picking things apart to see how they work. Others may like theabsolute rigor that Metamath offers. Someone new to logic and settheory, who is still developing the mathematical maturity needed tofollow informal textbook proofs, may find some reassurance in Metamath'sstep-by-step breakdown. And anyone who appreciates the austere eleganceof formal mathematics for its own sake might enjoy just casuallybrowsing through the proofs for their aesthetic appeal.

Q: I already havean abstract mathematics background. How can I grasp the keyideas 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 largestnumbers are usually the ones you want to look at first. The steps withsmaller numbers are typically logic "glue" to tie them together. Thecolors follow roughly the rainbow colors as the statement numberincreases, so that the largest numbers tend to stand out from theothers.With a little practice, this feature,together with the gray indentation levels showingthe tree structure, should help you figure out the "important" steps so that you couldwrite down an informal version of the proof ifyou wanted to.
(By the way, it's best not to use the colored numbersto reference theorems in an archived discussion, since they changewhen new theorems are inserted at an earlier point in the database.)

Q: What does theMetamath language look like?
A: The precise technical specification of the language is givenin Section 4.1 (p. 112) of the Metamath bookand is about 4 pages long. A simple example is given in Section 2.2.2 (p. 40).Compare this source screenshot withthe generated web page. But youdon't have to know or even look at the language if you just wantto follow the proofs on these web pages.
The metamath program andmmj2 are the main tools for working withthe 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 acouple dozen axioms, effectively give you the building blocks for all ofmathematics."Bob Solovay wrote a nicely commentedpresentation of Peano arithmetic in the Metamath language, peano.mm, that is worth reading as astand-alone file.

Q: What otherprograms have been written for the Metamath language?
A: Over a dozen proof verifiers for the Metamath language havebeen written and are listed atKnown Metamath proof verifiers.Also, several proof languages have been based on Metamath, andthe software and other documentation for these can be found underMetamath-related programs.

Q: How confidentcan I be in the proofs?
A: You can be extremely confident that the proofs follow fromtheir axioms.All reasoning is done directly in the proof itselfrather than by algorithms embedded in the verification program.Computer verification programs never get tired and rigorously check every step.There is the risk that a verifier has a programming bug, but thisis countered by the Metamath language's small size(this simplicity reduces the likelihood of such bugs) andby using multiple independently-implemented verifiers(since it is unlikely that all verifiers will have the same kind of bug).For example, theMetamath Proof Exploreris routinely checked by 4 independent verifiers:metamath (a C verifier by Norm Megill),mmj2 (a Java verifier by Mel O'Cat and Mario Carneiro),smetamath-rs (a high-speed Rust verifier by Stefan O'Rear), andcheckmm (a C++ verifier by Eric Schmidt).In addition, the databases are public and can easily be inspected;the hypertext links in generated proofs make it especially easy to movefrom one theorem to the next.Metamath enables an extremely rigorous form of peer review.

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

Q: Are there othersites that formalize math from its foundations?
A: Another project that aims to rigorously formalize and verifymath is Mizar [retrieved 4-Aug-2016]. Itis intended to appeal to professional mathematicians and requires acertain mathematical maturity to be able to follow its proofs. It triesto mimic mathematical proofs they way they are normally published,whereas Metamath shows you every little detail.
Some other well-known interactivetheorem provers are HOL Light[retrieved 4-Aug-2016], Isabelle[retrieved 4-Aug-2016], and Coq [retrieved 4-Aug-2016].There are a few languages based on or derived from Metamath, e.g.,Raph Levien has developed a related language called Ghilbert [retrieved 4-Aug-2016]that strives to improve upon Metamath by guaranteeing the soundness ofdefinitions and providing features useful for collaborative work.Freek Wiedijk wrote an interesting collection of notes [retrieved 4-Aug-2016]comparing several mathematical proof languages. His book, TheSeventeen Provers of the World [retrieved 4-Aug-2016] (PDF, 0.6MB), compares theproofs that the square root of 2 is irrational in 17 proof languages,including Metamath (theorem sqrt2irr).TheMetamath 100 page shows metamath's progressinFormalizing 100 Theorems(a challenge set of theorems for math formalization systems).
Unlike most other systems, Metamathattempts to use the minimum possible framework needed to expressmathematics and its proofs. Other systems do not consider that aspectnecessarily important, and their underlying computer programs can belarge and complex in order to perform mathematical reasoning at a higherlevel. Metamath's proofs are often quite long compared to those ofother systems, but they are completely transparent with nothing hiddenfrom the user. All reasoning is done directly in the proof itselfrather than by algorithms embedded in the verification program.Metamath is unique in this sense, offering an alternative approach forthose attracted to its philosophy of simplicity.

Q: Howcan I contribute to Metamath?
A:We'd be delighted to get your contributions!The Metamath community has a large set of inter-related projects, so you first need to determine whichspecific project you want to contribute to.Here are some common cases:If you're contributing to "set.mm" (the set of proofs which startsfrom ZFC set theory axioms and shown in the "Metamath Proof Explorer"),the recommended approach is to use its GitHub repository at https://github.com/metamath/set.mm(at least as a starting point). For detailed instructions on usingGitHub for this project, readGetting started with contributing andCONTRIBUTING.md.As an alternative to submitting GitHub pull requests (if you don't want togo through that learning curve in the beginning), you canemail patch files (differences) toNorm Megill orMario Carneiro or evenpost to theMetamath mailinglist.If you want to patch the mmj2 program (the editor/GUI proofassistant written in Java by Mel O'Cat and enhanced by Mario Carneiro),email Mario Carneiro and/or getyourself added to https://github.com/digama0/mmj2.If you want to patch the metamath.exe program (the original toolimplementation written in C), send your patch as a "unified diff" ("diff-u") via email to NormMegill.If you want to modify a web page,send email to Norm Megill.When in doubt, ask or post your proposal tothe metamathmailing list,and/or privately emailNorm Megill andMario Carneiro.

@Book{metamath,
author = {Norman D. Megill},
author = {David A. Wheeler},
title = {Metamath: A Computer Language for Mathematical Proofs},
year = {2019},
publisher = {Lulu Press},
address = {Morrisville, North Carolina},
note = {{\tt http://us.metamath.org/downloads/metamath.pdf}},
}
metamath.tar.bz2 (14 MB) ormetamath.tar.gz (17 MB) ormetamath.zip (17 MB) Description: The metamath program (version 0.198 7-Aug-2021), which is an ASCII-based ANSI C program with a command-line interface. It was used (along with mmj2 below) to build and verify the proofs in the Metamath Proof Explorer, and it generated 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 "readset.mm". For Linux/MacOSX/Unix, compile with the command "gcc*.c-ometamath" inside the "metamath" directory, then type "./metamathset.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 wantthe main (set.mm) database: 1. Download theMetamath programmetamath.exe (0.5MB)2. Download the set.mm database (25MB) into the same folder.3. Double-click on "metamath.exe" and type "readset.mm".4. To uninstall, just delete these two files. Nothing else is touchedon your system.On MacOSX, select the Terminalapplication from Applications/Utilities to get to the commandline. On recent versions of MacOSX, you need to install gccseparately. Typing "whereis gcc" will return "/usr/bin/gcc" if it isinstalled. The XCode package is typically used to install it,but it can also be installedwithout XCode[retrieved 4-Aug-2016].On Linux/MacOSX/Unix, theMetamath program will bemore pleasant to use if you run it inside of rlwrap[retrieved 30-Mar-2019],which provides up-arrow command history and othercommand-line editing features. After you install rlwrap per itsinstructions(see rlwrap installation[retrieved 30-Mar-2019] for macOS), invoke the Metamath program with "rlwrap ./metamathset.mm". (Thanks to Marnix Klooster for bringing rlwrap to myattention. The Windows version of the Metamath program, by the way, wascompiled with lcc, which has some similar featuresbuilt-in.)See the README.TXT file foradditional information. mmj2.zip(7.2 MB) (latest version, 2.4.1 26-Jan-2016, maintained byMario Carneiro)
mmj2-orig.zip(Mel O'Cat's last official version, 11-Oct-2011)
https://github.com/digama0/mmj2(development repository) Description: Mel O'Cat andMario Carneiro'smmj2 GUI Proof Assistant forthe Metamath language. Includes thorough file validation andproof verification, syntactic parsing of Metamath formulasand many other features.Instructions: Downloadmmj2jar.zip, unzip and read theenclosed documentation.David A. Wheeler produced two introductoryvideos "Introduction toMetamath mmj2" [retrieved 1-Aug-2016] and"Creating Functions in Metamath" [retrieved 1-Aug-2016].Some documentation is also available at the (now archived) AsteroidMeta wikimmj2 [retrieved 24-May-2016].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).
3a. The first line will read "LoadFile,set.mm"; change it if necessary to point to your set.mm file.
3b. Add the following 2 lines immediately above the last line that reads "RunProofAsstGUI" (to improve automation in the proof assistant):
ProofAsstDeriveAutocomplete, yes
ProofAsstUseAutotransformations, yes,no,yes
3c. Add the following 2 lines to the end of the file (to ensure set.mm definitions are sound):
RunMacro,definitionCheck,ax-*,df-bi,df-clab,df-cleq,df-clel
*done
4. Edit C:\mmj2jar\mmj2.bat. Change "-Xmx256M" to "-Xmx512M" (to increase heap space for current set.mm size). Change "C:\metamath" to a directory that exists (to store .mmp worksheets).
5. Start - All Programs - Accessories - Command Prompt
6. Type: java then ENTER. If the response is "'java' is not recognized...",you need to install the Java runtime system fromjava.com[retrieved 11-May-2016], then exit and reenter the Command Prompt.
7. Type:
CD C:\mmj2jar
mmj2.bat
Notes:The eimm export-import programlinks the mmj2 and Metamath proof assistantswithout exiting from either program, giving you the features of bothduring proof development. The mmj2 directorylisting also has the source code, older releases, and MD5 checksums. mpeuni.tar.bz2 (70 MB) ormpeuni.tar.gz (140 MB) ormpeuni.zip (180 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 GIF version of the pages.) Instructions: Extract all files (around 35,000) into a directory called "mpeuni". The home page is the file "mmset.html". You will need about 3.5 GB of free space. qleuni.tar.bz2 (1 MB) orqleuni.tar.gz (2 MB) orqleuni.zip (4 MB) Description: The complete set of Quantum Logic Explorer web pages. Instructions: Extract all files (around 1,000) into a directory called "qleuni". The home page is the file "mmql.html". mmsolitaire.tar.bz2 (0.2 MB) ormmsolitaire.tar.gz (0.2 MB) ormmsolitaire.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) orsymbols.tar.gz (0.3 MB) orsymbols.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 thecomments at the top of the program listing. eimm.zip (0.1 MB) Description: An experimentalproof export-import program (version 0.08 23-Mar-2021) thattranslates incomplete proofs in progress between the Metamath program's CLI Proof Assistantand Mel O'Cat's mmj2GUI Proof Assistant, without exiting from either proofassistant, giving you the features of both assistants during proofdevelopment.Instructions: Extract all filesinto a directory called "eimm". See the readme.txt file for detailedinstructions. A pre-compiled Windows binary is provided; gcc is requiredto compile for Linux/MacOSX/Unix.

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

Status: There are no known bugs.The development of this prototype is believed to be complete. The onlychange in the future might be to incorporate the import-exportalgorithms 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 FinitelyAxiomatized Formalization of Predicate Calculus with Equality," whichprovides the theoretical basis for Metamath and is referenced on theMetamath Proof Explorer pages. [This PDF file was generated from the LaTeXsource file finiteaxiom.tex (0.1 MB).] The correspondencebetween the axioms in this paper and the ones in theset.mm database is described inAppendix 8 of theMetamath Proof Explorer Home Page.See technical note 1 forsome additional notes. 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) orquantum-logic.tar.gz (0.1 MB) orquantum-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 usedfor the papers and will reproduce the papers' results exactly.Each .c file is a stand-alone program. After compiling (underLinux/Cygwin/MacOSX/Unix) with "gcc program.c -o program",type "./program --help" for instructions. metamathsite.tar.bz2 (111 MB) ormetamathsite.tar.gz (116 MB) ormetamathsite.zip (117 MB) Description:A mirror of the entire Metamath web siteincluding all thedownloads listed above (that aren't external links).This can be useful if you have a slow connectionor want to browse the site off-line. A script buildsthe site from source files and requires a Linux/MacOSX/Unix operatingsystem (or the free Cygwin[retrieved 4-Aug-2016]for Windows).About 9 GB of disk space will be needed. Instructions:Extract all files into a directory called "metamathsite". Go to thatdirectory then type "./install.sh". Thismay 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) isC:\tmp\metamathsite.On MacOSX, selectthe Terminal application fromApplications/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 thataccompanies the download for more detailedinstructions.Another way to install your local copy is with rsync (onLinux/MacOSX/Unix or Cygwin). The download will be compressed to about2GB and automatically expanded to about 3.5GB. Create and go to themetamathsite directory, then type (including the last period):
rsync -vrltS -z --delete --delete-afterrsync://rsync.metamath.org/metamath .
Rerunning this same commandperiodically will also keep your copy updated, downloading only thefiles that changed. Note that you need twice the disk spaceduring rsync, i.e. 7GB. A third way to install your local copy is with wget (see the Download and Extraction Help below). The fulluncompressed 3.5GB site will be downloaded, so it will take a long time,depending on your connection speed. Create and go to the metamathsitedirectory, then type:
wget -nH --mirror"http://us.metamath.org/index.html"If you would like to set up a mirror site for public access, readthe instructions in mirror.txt.

Downloading Some browsers mayhave problems downloading large binary files. The free wget [retrieved4-Aug-2016] program downloads correctly and is available for allplatforms including Windows. Here are the instructions for Windows:Go to http://www.filewatcher.com/m/wget-1.8.2b.zip.278487-0.html[retrieved 4-Aug-2016] (or another mirror site) and download wget-1.8.2b.zip(272kB). Extract the file called WGET.EXEinto the folder you will be using for your downloads. The other filesare 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 clickOK.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. Thentype
cd folder
and pressEnter, where folder is the folder (without the drive letter andcolon) you will be using for your downloads.Type
wget "url"
(include the quotes around url) and press Enter, whereurl is the URL (internet address, which begins with "http://" or"ftp://") of the .tar.bz2 or other file you want to download. Mostbrowsers can copy a URL from a web page display, for example byright-clicking on the link and selecting "Copy Shortcut" or "Copy LinkLocation", which you can then paste into the wgetargument. To paste, right-click on the top of the command windowand select Edit - Paste.If you have trouble retrieving FTP files because you are behinda network firewall, try typing
wget--passive-ftp "url"Extracting Toextract .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 -tjfxxx.tar.bz2 | more"; press the space bar to show the next pageand "q" to quit the preview. (On MacOSX, select the Terminalapplication from Applications/Utilities to get to the commandline.)

To extract .tar.gz files in Linux/MacOSX/Unix, use "tar -xzfxxx.tar.gz". To preview them, use "tar -tzf xxx.tar.gz |more".

To extract .zip files in Linux/MacOSX/Unix, use "unzipxxx.zip". To preview them, use "unzip -l xxx.zip |more".

To extract .tar.gz and .zip files in Windows, you can useWinZip, WinAce, or WinRAR, among others. Of these, I have been toldthat only WinRAR can extract .tar.bz2 files. Recent Windows versionswill open .zip files automatically. If you have the free Cygwin [retrieved 4-Aug-2016] installed,you can usethe Unix commands above for .tar.bz2, .tar.gz, and .zip files.

Text filesTheASCII (text) files in the downloads are in Unix format, which uses abare line-feed character at the end of each line. This may cause themto display improperly in some Windows text editors such as Notepad,which requires a carriage-return/line-feed combination. The better texteditors don't have this problem, but if you need to convert the format,a free program that has been recommended for Windows isToX[retrieved 4-Aug-2016]. (For Linux/MacOSX/Unix, use the command:sed -e 's/$/\r/' unixfile windowsfile. To go back, use thecommand: tr -d '\015' windowsfile unixfile.)

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