New Foundations Explorer 
Constructs mathematics from scratch, starting from
Quine's NF set theory axioms.
Updated 17Apr2015.



HigherOrder Logic Explorer 
Starts with HOL (also called simple type theory) and derives equivalents to
ZFC axioms, connecting the two approaches.
Updated 12Jul2015.



Intuitionistic Logic Explorer 
Derives mathematics from a constructive point of view, starting from
axioms of intuitionistic logic.
Updated 13Nov2017.



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 11Sep2009.



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 8Jun2014.



Metamath Solitaire  A Java
applet
that demonstrates simple proofs.
Builtin axiom systems
include ZFC; modal, intuitionistic, and quantum logics; and Tarski's
plane geometry.
Updated 14Mar2018.



Metamath Music Page  Strictly
for fun. You can listen
to what mathematical proofs "sound" like!
Updated 3Feb2017.



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: How can I ask
questions or discuss Metamathrelated topics?
A: The Metamath
Google Group [retrieved 4Aug2016] mailing list is being used for
discussion about Metamath. If you have questions, that is a good place
to ask them. (The AsteroidMeta [retrieved 4Aug2016] wiki was used for many older
Metamath discussions, but is no longer available. Archived discussions
such as this one can be found on archive.org.)
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.
Obviously knowledge of mathematics
is important.
For a nice independent introduction to logic,
see Hirst and
Hirst's A Primer
for Logic and Proof [retrieved 27Sep2017] (PDF, 0.5MB); compare its axioms to ours.
Wikipedia has an overview of set theory
[retrieved 4Aug2016].
The video series
"Introduction to Higher Mathematics" by Bill Shillito
[retrieved 27Sep2017] may also be helpful.
You can experiment with simple
proofs in the Metamath Solitaire
applet.
To actually create real metamath proofs, you'll want to
download a tool.
A common tool is mmj2.
David A. Wheeler produced an introductory video, "Introduction to
Metamath & mmj2" [retrieved 4Aug2016].
Q: Will Metamath
help 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 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 CrossReference 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
stepbystep 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 and
mmj2 are the main tools 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."
Bob Solovay wrote a nicely commented
presentation of Peano arithmetic in the Metamath language, peano.mm, that is worth reading as a
standalone file.
Q: What other
programs have been written for the Metamath language?
A: Over a dozen proof verifiers for the Metamath language have
been written and are listed at
Known Metamath proof verifiers.
Also, several proof languages have been based on Metamath, and
the software and other documentation for these can be found under
Metamathrelated programs.
Q: How confident
can I be in the proofs?
A: You can be extremely confident that the proofs follow from
their axioms.
All reasoning is done directly in the proof itself
rather 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 this
is countered by the Metamath language's small size
(this simplicity reduces the likelihood of such bugs) and
by using multiple independentlyimplemented verifiers
(since it is unlikely that all verifiers will have the same kind of bug).
For example, the
Metamath Proof Explorer
is routinely checked by 4 independent verifiers:
metamath (a C verifier by Norm Megill),
mmj2 (a Java verifier by Mel O'Cat and Mario Carneiro),
smetamathrs
(a highspeed Rust verifier by Stefan O'Rear), and
checkmm (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 move
from 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 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 [retrieved 4Aug2016]. 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.
Some other wellknown interactive
theorem provers are HOL Light
[retrieved 4Aug2016], Isabelle
[retrieved 4Aug2016], and Coq [retrieved 4Aug2016].
There are a few languages based on or derived from Metamath, e.g.,
Raph Levien has developed a related language called Ghilbert [retrieved 4Aug2016]
that strives to improve upon Metamath by guaranteeing the soundness of
definitions and providing features useful for collaborative work.
Freek Wiedijk wrote an interesting collection of notes [retrieved 4Aug2016]
comparing several mathematical proof languages. His book, The
Seventeen Provers of the World [retrieved 4Aug2016] (PDF, 0.6MB), compares the
proofs that the square root of 2 is irrational in 17 proof languages,
including Metamath (theorem sqr2irr).
The
Metamath 100 page shows metamath's progress
in
Formalizing 100 Theorems
(a challenge set of theorems for math formalization systems).
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.
Q: How
can I contribute to Metamath?
A:
We'd be delighted to get your contributions!
The Metamath community has a large set of interrelated projects, so you first need to determine which
specific project you want to contribute to.
Here are some common cases:
 If you're contributing to "set.mm" (the set of proofs which starts from 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).
You can submit pull requests, post to the
metamath mailing list,
or simply email patch files (differences) to
Norm Megill or
Mario Carneiro.
 If you want to patch the mmj2 program (the editor/GUI proof assistant written in Java by Mel O'Cat and enhanced by Mario Carneiro), email Mario Carneiro and/or get yourself added to https://github.com/digama0/mmj2.
 If you want to patch the metamath.exe program (the original tool implementation written in C),
send your patch as a "unified diff" ("diff u")
via email to Norm Megill.
Note that although metamath.exe does come with a copy of set.mm, it's not necessarily the current version.
 If you want to modify a web page,
send email to Norm Megill.
When in doubt, ask or post your proposal to
the metamath mailing list,
and/or privately email
Norm Megill and
Mario Carneiro.
Downloads
 metamath.pdf
(1.3 MB)
 Description: The
Metamath book (211 pp.), which
provides an indepth understanding of the Metamath language
and program. The first
part of the book also includes an easytoread 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
[retrieved 4Aug2016] of the Metamath book
(ISBN 9781411637245) 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 Press},
address = {Morrisville, North Carolina},
note = {{\tt http://us.metamath.org/downloads/metamath.pdf}},
}
New 4Jul2011 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 (10 MB) or
metamath.tar.gz (12 MB) or
metamath.zip (12 MB)
 Description: The
metamath program (version 0.161 2Feb2018), which is an
ASCIIbased ANSI C
program with a commandline 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, doubleclick 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 indepth 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 (25MB) into the
same folder.
3. Doubleclick 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[retrieved 4Aug2016].
 On Linux/MacOSX/Unix, the
Metamath program will be
more pleasant to use if you run it inside of
rlwrap
[retrieved 2Jan2018],
which provides uparrow command history and other
commandline editing features. After you install rlwrap per its
instructions
(see rlwrap installation
[retrieved 2Jan2018] for macOS),
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
builtin.)
 See the README.TXT file for
additional information.

mmj2.zip
(7.2 MB) (latest version, 2.4.1 26Jan2016, maintained by
Mario Carneiro)
mmj2orig.zip
(Mel O'Cat's last official version, 11Oct2011)
https://github.com/digama0/mmj2
(development repository)
 Description: Mel O'Cat and
Mario Carneiro'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.
David A. Wheeler produced two introductory
videos "Introduction to
Metamath & mmj2" [retrieved 1Aug2016] and
"Creating Functions in Metamath" [retrieved 1Aug2016].
Some documentation is also available at the (now archived) Asteroid
Meta wiki
mmj2 [retrieved 24May2016].
 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*,dfbi,dfclab,dfcleq,dfclel
*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 from
java.com
[retrieved 11May2016], then exit and reenter the Command Prompt.
7. Type:
CD C:\mmj2jar
mmj2.bat
 Notes:
 The eimm exportimport 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.

mpeuni.tar.bz2 (70 MB) or
mpeuni.tar.gz (140 MB) or
mpeuni.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 22,000) into a directory
called "mpeuni". The home page is the file "mmset.html". You will need
about 1.5 GB of free space.

qleuni.tar.bz2 (1 MB) or
qleuni.tar.gz (2 MB) or
qleuni.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) 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 27Jan2013)
(previous version)
 Description: Raph Levien's
independentlywritten Python
proof verifier for the Metamath language.
 Instructions: See the
comments at the top of the program listing.
 eimm.zip (0.03 MB)
New 18Apr2006
 Description: An experimental
proof exportimport program (version 0.07 18Oct10) 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 precompiled Windows binary is provided; gcc is required
to compile for Linux/MacOSX/Unix.
Metamath program's Proof Assistant (MMPA> 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 importexport
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).]
See technical note 1 for
some additional notes on this paper.

weakd.pdf (0.2 MB)
 Description: The article
"Weaker DComplete 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.

quantumlogic.tar.bz2 (0.05 MB) or
quantumlogic.tar.gz (0.1 MB) or
quantumlogic.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 "quantumlogic". 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.
Each .c file is a standalone program. After compiling (under
Linux/Cygwin/MacOSX/Unix) with "gcc program.c o program",
type "./program help" for instructions.

metamathsite.tar.bz2 (60 MB) or
metamathsite.tar.gz (70 MB) or
metamathsite.zip (70 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 offline. A script builds
the site from source files and requires a Linux/MacOSX/Unix operating
system (or the free Cygwin
[retrieved 4Aug2016]
for Windows).
About 7 GB of disk space will be needed.
 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 deleteafter
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 [retrieved
4Aug2016] program downloads correctly and is available for all
platforms including Windows. Here are the instructions for Windows:
 Go to http://www.filewatcher.com/m/wget1.8.2b.zip.2784870.html
[retrieved 4Aug2016] (or another mirror site) and download wget1.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
driveletter: and press Enter, where driveletter (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
rightclicking on the link and selecting "Copy Shortcut" or "Copy Link
Location", which you can then paste into the wget
argument. To paste, rightclick 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
passiveftp "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 [retrieved 4Aug2016] 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 linefeed 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 carriagereturn/linefeed 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
[retrieved 4Aug2016]. (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 viceversa on Linux/MacOSX/Unix).
Note: Some of the links in the section below are obsolete. Let me
know if you have current links. NM 16Feb2013

Directories 
Wikipedia 
Drexel University's Math Forum Internet
Mathematics Library (another
mention) 
Government of Australia
Education Portal 
Encyclopædia Britannica "approved
iGuide site" (Oct. 11, 2006) (free
set theory
full text article) 

Awards 
The Golden House Sparrow Award:
Site of the Day (Jul. 20, 2000) (check out their eclectic current
page) 
Scout
Report for Science and Engineering Selection (Jul. 19, 2000) 
Knot a Braid
of Links "Cool
math site of the week" (Jul. 713, 1998) 
Rated by JARS (Apr. 26, 1998) 
This page was last updated on
18May2018.
