This page collects supplementary material related to Metamath. If you have
a topic you wish to add, contact Norm Megill.
Contents of this page
- The Metamath 100 list
- CICM 2016:
Prime Number Theorem (PDF slides)
by Mario Carneiro, with an informal exposition of the related
Dirichlet's theorem [retrieved 4-Aug-2016].
Models for Metamath (PDF slides)
by Mario Carneiro; the paper is also available at
Google Groups discussion [retrieved 4-Aug-2016].
- CICM 2015:
implies AC, a Metamath Formalization (YouTube
video) [retrieved 19-Jul-2015]
(PDF paper) [retrieved
19-Jul-2015] by Mario
Arithmetic in Metamath
Case Study: Bertrand's Postulate (CICM 2015) (YouTube
video) [retrieved 19-Jul-2015]
(PDF paper) [retrieved
19-Jul-2015] by Mario Carneiro.
- "Collapsible proof demo"
A click on the magnifying glass will
expand, collapse, show substitution, hide substitution depending
on context. Other than an interface that takes getting used to,
this is a very nice proof-of-concept demo showing features
that are possible. Feel free to take over this project to
enhance it. Personally, I would prefer a separate button for
collapse/expand similar to Windows Explorer and would also prefer
to see the proof
fully expanded on loading.
AsteroidMeta metamath and mmj2 archived wiki
discussions (read-only; partial recovery to Nov. 2008).
Missing pages are
sometimes on archive.org e.g. archive.org
page for metamath (but LaTeX math image files may be missing
after 2013 or so).
- grammar-ambiguity.txt -
a proof of the unambiguity of set.mm's grammar by Mario Carneiro
- Overview of Metamath
presentation by Norm Megill at Institut Henri Poincaré (2014)
- Open problems and miscellany discussed
at 2003, 2004, and 2005 Argonne workshops
- Shortest known proofs of the
propositional calculus theorems from
Sean B. Palmer has created
[retrieved 6-Oct-2017] to verify these
independently and also to search for shorter proofs.
- Editor screenshots and syntax highlighting
- Robert Solovay's Metamath database source file
peano.mm (Peano arithmetic)
- Other Metamath database source files:
miu.mm (Hofstadter's MIU-system),
(William McCune's unification stress test),
(toy formal system)
- Current web usage statistics (us.metamath.org mirror only)
summary by month
with links to details;
current raw Webalizer data
- College and university visitors to the
Metamath site in Jan. 2004 (based on old server log)
- Czur ET-16 scanner notes
(for NM's convenient reference; probably not interesting to others)
Known Metamath proof verifiers
This proof verifiers in this list sometimes have a local archived copy.
When an external link is also available, check it to see that you
have the most recent version. If you have or know of a more recent
version or updated external link, let me know so I can update it.
- metamath (current version) -
the original Metamath proof verifier and proof assistant
(written in C by Norman Megill)
- Sean B. Palmer has a
[retrieved 6-Oct-2017] that runs the metamath program
"When you load that page it emulates an entire Linux stack running on
an OpenRISC CPU simulator written by Sebastian Macke. I added Metamath
to its filesystem, compiled it, and set it up so that it runs in
screen. It takes about 30 seconds to boot to Metamath on this page in
Firefox and Chrome for me... To verify all proofs took my browser about
half an hour. But at least this may serve as a curiosity."
- mmj2 proof assistant and verifier
(written in Java by Mel O'Cat; enhanced and maintained by Mario Carneiro).
wiki page [retrieved 3-Aug-2016] as of 2011.
[retrieved 13-Jul-2017] - a Metamath proof
verifier written in the Scala
language as part of an ongoing Metamath -> MM
[retrieved 12-Jun-2016] - a Metamath proof verifier written in the Julia
language, by Dan Getz. See also
https://juliaobserver.com/packages/Metamath [retrived 9-Jul-2017].
- mmamm.m (29-Mar-2016) -
A verifier written in the Mathematica language by Mario Carneiro, who says
it "is only 74 lines (give or take, lines in Mathematica
are kind of a moving target) and 2885
characters. Of course it is not
very efficient, and it also does not like local $v declarations (which I
think are not in set.mm anymore), but it will catch all
the important errors. It also works with both normal and compressed proofs."
[retrieved 6-Sep-2015] -
the smm, smm2, smm3 Metamath proof verifiers
goal of providing another proof assistant. By using multiple threads,
smm3 verifies set.mm in 0.7s on a 2-core, 2-way SMT Intel i5
1.6GHz CPU as of June 18, 2016. See this
Google Groups post [retrieved 21-Jun-2016].
- MM Tool [retrieved 6-Sep-2015] -
a Metamath proof verifier and editor that runs in a browser
to Metamath that summarizes the basics of the Metamath language,
which you may find useful.
- Igor [retrieved
24-Sep-2015] - A proof assistant for Metamath, specialized for set.mm
(written in a custom language by Drahflow; in progress)
- mmverify.py (27-Jan-2013) -
the mmverify Metamath proof verifier
(written in 350 lines of Python by Raph Levien)
hmm.zip (3-Nov-2006) - the hmm
Metamath proof verifier (written in 400 lines of Haskell by Marnix
Klooster). External link: hmm [retrieved
- verify.lua (21-Oct-2006) -
a Metamath proof verifier
(written in 380 lines of Lua by Martin Kiselkov; needs 40 min
to verify set.mm, but provides an interesting example for learning Lua).
External link: verify.lua
- Verifier.cs (29-Oct-2010) - a
Metamath proof verifier (written in 550 lines of C# by Chris Capel).
External link: verifier.cs
- checkmm.cpp (9-Dec-2010) -
the checkmm Metamath proof verifier
(written in C++ by Eric Schmidt)
- smetamath-rs -
Metamath system engine [retrieved 3-Aug-2016] (written in Rust by Stefan
(16-Jul-2017) - a simple Metamath proof checker [retrieved 15-Aug-2016]
(written in Ada by Tony Häger). It should probably be considered to be
under development; see this this Google
Group message for its limitations. A zip download is also attached
to that message.
Other tools for Metamath
- MILP: Math
is like a puzzle! [retrieved 18-Feb-2017] - Milpgame is an
application by Filip Cernatescu in which you can demonstrate a given
statement using axioms and theorems and is based on Metamath. The site
has Metamath tests focused on the set.mm set theory file.
(Note: The program is freeware that runs on Windows.
It is not open source.)
[retrieved 22-Aug-2016] - a Metamath-specialized automated theorem prover
written in Python by Daniel Whalen. The paper describes using deep
learning to prove 14% of its test propositions from set.mm.
Other links: paper
[retrieved 22-Aug-2016], working
release [retrieved 22-Aug-2016].
[retrieved 15-Aug-2016], by David A. Wheeler, contains test cases
(positive and negative) for Metamath verifiers and automatically runs
them against a collection of verifiers. Last
execution run [retrieved 15-Aug-2016].
[retrieved 3-Aug-2016] - Metamath plugin for Eclipse IDE, with mmj2
in Java by Thierry Arnoux).
Google Groups discussion [retrieved 10-Jul-2016].
plugin for Eclipse based on Xtext
[retrieved 3-Aug-2016] - Metamath plugin for Eclipse IDE (written
in Xtext by Marnix Klooster).
Google Groups discussion [retrieved 22-Oct-2015].
- completeusersproof (14-Sep-2016,
updated 4-Oct-2017) - Alan Sare's completeusersproof software that
enhances mmj2 for certain kinds of proofs. Documentation can be found
in the __README.TXT file in the zip file (also reproduced here). Alan can be
contacted directly for questions: alansare at alumni dot cmu dot
- mmide.zip (15-Aug-2006) - mmide
provides a graphical user interface for displaying the output of the
Metamath program commands (written in Python by William Hale). External
link: mmide [retrieved 3-Aug-2016].
- gh_verify [retrieved
3-Aug-2016] - a verifier for the Ghilbert language (written in Python by
(14-Jan-2007) - a verifier for the Ghilbert language (written in C by
Dan Krejsa; loads and verifies the translated 2008 set.mm in 500 ms).
- bourbaki.zip (20-Dec-2006) - a
proof checker for Bourbaki, a custom Lisp-like language related to
Metamath (written in Common Lisp by Juha Arpiainen). External link: Bourbaki proof checker [retrieved 3-Aug-2016].
- jhilbert-8.zip (24-Jun-2009) -
JHilbert (written in Java by Alexander Klauer), a proof verifier for
collaborative theorem proving "in the spirit of Ghilbert" and the engine
behind Wikiproofs [retrieved
3-Aug-2016] External links: JHilbert [retrieved 3-Aug-2016],
JHilbert [retrieved 3-Aug-2016].
(10-Apr-2013) - Russell Math verifier (written in C++ by D. Yu Vlasov).
Built upon Metamath as a high level superstructure with an automatic
proving facility, described in a paper [retrieved 3-Aug-2016]
(in Russian) and reviewed here [retrieved 3-Aug-2016]. External link: rusellmath.org [retrieved 3-Aug-2016]
SourceForge page: Mathematics
Development Language [retrieved 3-Aug-2016].
Mathematica program to generate
arithmetic proof steps
(11-Jul-2015) Mario Carneiro has developed a
reference implementation of a Mathematica program, arithmetic.nb, to fill in missing
arithmetic steps in an mmj2 proof worksheet. An example of its use was
for the proof of log2ub, which proves
that log(2) < 253/365. The starting worksheet log2ub-orig.mmp has 150 steps, 12
of them incomplete (the most complicated unproven assertion being
53057*365 < 253*(3^7)*5*7). The Mathematica program processes this
file in about 0.25 seconds to produce a completed proof worksheet (log2ub.mmp) with 716 steps.
Reading this worksheet into mmj2 generates the final compressed proof of
8167 bytes, which can be decreased to the current 6942 bytes by a
separate proof optimization algorithm (the 'minimize' command in the
Study of complex number axiomatization
In June 2012,
Eric Schmidt discovered that two of our
Axioms for Complex Numbers,
ax-addcom (now addcom) and
ax-0id (now addid1), were redundant.
His results are described in
which also includes independence results for the remaining
In addition, ax-1id (now mulid1)
for complex numbers can be
weakened to ax-1rid for reals.
In Jan. 2013,
Scott Fenton formalized Eric's work, resulting in
23 instead of 25 axioms for real and
complex numbers in set.mm. The
Axioms for Complex Numbers
page has been updated with these results.
An interesting part
of the proof, showing how commutativity of addition follows from
other laws, is in
addcomi. Gérard Lang pointed
out that this
holds for rings generally, which is now shown by theorem
Natural deduction in Metamath
In July 2014,
Mario Carneiro presented a talk, "Natural Deduction in the
Metamath Proof Language," at the
6PCM conference [retrieved 12-Jul-2015]. It describes the
natural deduction emulation method (prefixing hypotheses and theorems
") that we
now commonly use in set.mm to achieve significant savings in proof sizes.
natded.pdf for slides and
natded.mp3 for audio.
The links in this section are provided as a courtesy to
correspondents who have requested them. They may be commercial in
nature and may or may not be related to Metamath. The Metamath project
does not necessarily endorse these links and receives no compensation
for posting them. They may be removed by us at any time for any reason.
- Tyson Stevens requested a link to Online
Colleges that Offer Laptops and wrote, "EDsmart offers a student
laptop guide with information about online colleges that offer laptops
and iPads to their students. It also provides a comprehensive guide to
what to look for in a laptop for college students. EDsmart itself is also a great
resource for students." (Added 20-Sep-2017)
- Branden Passwaters from OnlineCollegePlan requested a link to
the Top 100 Best Online Colleges. (Added 21-Aug-2017)
- Lauren Young requested a link to The Best
Online Colleges of 2016 and wrote, "These resources can help
students, their families and educators understand the online education
landscape as well as breaking down top online programs across the United
States." (Added 6-Jul-2016)
- Francine Millar requested a link to
Affordable Online Colleges for 2016
and wrote, "Not-for-profit public and private colleges and university
ever before are incorporating online degree programs. This trend is
creating more opportunities for students to pursue their college
education and at the same time making it much more affordable.
Unfortunately, many students and their parents are not aware of this and
part of the reason is because much of the news that we hear today about
online education is related to for-profit schools. For this reason, the
team at The Simple Dollar has published an investigative review of the
most affordable online programs available based on the US News College
Ranking report - taking into consideration only reputable and high
quality education that most people would consider." (Added 6-Jul-2016)
- Claire Castillo requested a link to
and wrote, "2016 is an exciting year for education as
most public and private not-for-profit colleges and universities in
California are incorporating online degree programs. Knowing that
students and families are faced with trying to figure out the best
educational route to take, OnlineColleges.net
has refocused their site and its resources to provide an investigative
review of the online education landscape and critically evaluate the
best program available, from quality to affordability. Most
importantly, they have provided scholarship information that students
can leverage to help finance their education." (Added 29-Mar-2016)
Claire Castillo also wrote,
"We are recently working with a new site to provide greater insight,
offer more information and most importantly sort through all the
different internship platform that are available to students. This
resource focused on what students should know before they apply, how
each of these platform work and how to find as many internship
opportunities as possible.
Here are the links to our guide:
- Matt Nelson requested a link to UptimePal and wrote, "UptimePal is a
website monitoring program that pings a given URL and checks for the
HTTP status code. If the code is 200, then it's considered 'up.' If a
different status code is detected, then it's considered 'down' and an
alert will be generated. Because UptimePal uses multiple datacenter
locations around the world, it also uses a complex monitoring frequency
algorithm in order to cycle those locations and correlate the
uptime/downtime calculations with individual monitoring locations...I
used Metamath to help with the formal verification process and
termination proofs while constructing the algorithm." Unfortunately, he
cannot share more details about the use of Metamath at this point
because of the proprietary nature of the algorithm. (Added 29-Mar-2016)