This page collects supplementary material related to Metamath. If you have
a topic you wish to add, contact Norm Megill.
Contents of this page

Other pages
External links

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).
Archived AsteroidMeta
wiki page [retrieved 3Aug2016] as of 2011.
 mmscala [retrieved 14Aug2016]  a Metamath proof
verifier written in the Scala
language as part of an ongoing Metamath > MM
import project
 Metamath.jl
[retrieved 12Jun2016]  a Metamath proof verifier written in the Julia
language, by Dan Getz.
 mmamm.m (29Mar2016) 
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."

smm
[retrieved 6Sep2015] 
the smm, smm2, smm3 Metamath proof verifiers
(written in JavaScript by Stefan O'Rear) with a longterm
goal of providing another proof assistant. By using multiple threads,
smm3 verifies set.mm in 0.7s on a 2core, 2way SMT Intel i5
1.6GHz CPU as of June 18, 2016. See this
Google Groups post [retrieved 21Jun2016].
 MM Tool [retrieved 6Sep2015] 
a Metamath proof verifier and editor that runs in a browser
(written in JavaScript by Ivan Kuckir)
 Igor [retrieved
24Sep2015]  A proof assistant for Metamath, specialized for set.mm
(written in a custom language by Drahflow; in progress)
 mmverify.py (27Jan2013) 
the mmverify Metamath proof verifier
(written in 350 lines of Python by Raph Levien)
 hmm.zip (3Nov2006)  the hmm
Metamath proof verifier (written in 400 lines of Haskell by Marnix
Klooster). External link: hmm [retrieved
3Aug2016]
 verify.lua (21Oct2006) 
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
[retrieved 3Aug2016]
 Verifier.cs (29Oct2010)  a
Metamath proof verifier (written in 550 lines of C# by Chris Capel).
External link: verifier.cs
[retrieved 3Aug2016]
 checkmm.cpp (9Dec2010) 
the checkmm Metamath proof verifier
(written in C++ by Eric Schmidt)
 smetamathrs 
Metamath system engine [retrieved 3Aug2016] (written in Rust by Stefan
O'Rear).
Other tools for Metamath
 MILP: Math
is like a puzzle! [retrieved 18Feb2017]  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 software is closed source, and I cannot vouch for
the integrity of the binaries.)

Holophrasm
[retrieved 22Aug2016]  a Metamathspecialized 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 22Aug2016], working
release [retrieved 22Aug2016].
 metamathtest
[retrieved 15Aug2016], 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 15Aug2016].

EMetamath
[retrieved 3Aug2016]  Metamath plugin for Eclipse IDE, with mmj2
inside (written
in Java by Thierry Arnoux).
Google Groups discussion [retrieved 10Jul2016].

Metamath
plugin for Eclipse based on Xtext
[retrieved 3Aug2016]  Metamath plugin for Eclipse IDE (written
in Xtext by Marnix Klooster).
Google Groups discussion [retrieved 22Oct2015].
 completeusersproof (14Sep2016,
updated 18Feb2017)  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
edu.
 mmide.zip (15Aug2006)  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 3Aug2016].
Metamathrelated programs
 gh_verify [retrieved
3Aug2016]  a verifier for the Ghilbert language (written in Python by
Raph Levien)
 shullivan0.05.zip
(14Jan2007)  a verifier for the Ghilbert language (written in C by
Dan Krejsa; loads and verifies the translated 2008 set.mm in 500 ms).
External link:
http://home.alamedanet.net/~dan.krejsa/shullivan/shullivan.html [broken
3Aug2016].
 bourbaki.zip (20Dec2006)  a
proof checker for Bourbaki, a custom Lisplike language related to
Metamath (written in Common Lisp by Juha Arpiainen). External link: Bourbaki proof checker [retrieved 3Aug2016].
 jhilbert8.zip (24Jun2009) 
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
3Aug2016] External links: JHilbert [retrieved 3Aug2016],
JHilbert [retrieved 3Aug2016].
 mdl0.8.772.tar.gz
(10Apr2013)  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 3Aug2016]
(in Russian) and reviewed here [retrieved 3Aug2016]. External link: rusellmath.org [retrieved 3Aug2016]
SourceForge page: Mathematics
Development Language [retrieved 3Aug2016].
Mathematica program to generate
arithmetic proof steps
(11Jul2015) 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 log2uborig.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
metamath program).
Study of complex number axiomatization
In June 2012,
Eric Schmidt discovered that two of our
Axioms for Complex Numbers,
namely
axaddcom (now addcom) and
ax0id (now addid1), were redundant.
His results are described in
schmidtcnaxioms.pdf
(LaTeX source
schmidtcnaxioms.tex),
which also includes independence results for the remaining
axioms.
In addition, ax1id (now mulid1)
for complex numbers can be
weakened to ax1rid 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
rngcom.
Natural deduction in Metamath
In July 2014,
Mario Carneiro presented a talk, "Natural Deduction in the
Metamath Proof Language," at the
6PCM conference [retrieved 12Jul2015]. It describes the
natural deduction emulation method (prefixing hypotheses and theorems
with
"
") that we
now commonly use in set.mm to achieve significant savings in proof sizes.
See
natded.pdf for slides and
natded.mp3 for audio.
Guest links
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 writes, "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 6Jul2016)
 Francine Millar requested a link to
Most
Affordable Online Colleges for 2016
and writes, "Notforprofit public and private colleges and university
more than
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 forprofit 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 6Jul2016)
 Claire Castillo requested a link to
OnlineColleges.net
and writes, "2016 is an exciting year for education as
most public and private notforprofit 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 29Mar2016)
 Matt Nelson requested a link to UptimePal and writes, "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 29Mar2016)