This page collects supplementary material related to Metamath. If you have
a topic you wish to add, contact Norm Megill.
Contents of this page
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)
- 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.
- mm-scala [retrieved 14-Aug-2016] - 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.
- 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
- 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
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 23-Mar-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 at any time for any reason.
- 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)