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
 The Metamath 100 list
 Big Proof 2017:
Systems
Based on Set Theory [retrieved 22Jan2018].
Mario Carneiro presents Metamath in the first
part of this talk.
 CICM 2016:
Prime Number Theorem (PDF slides)
(PPT)
by Mario Carneiro, with an informal exposition of the related
Dirichlet's theorem [retrieved 4Aug2016].
Models for Metamath (PDF slides)
(PPT)
(PDF paper)
by Mario Carneiro; the paper is also available at
arxiv.org
[retrieved 16Feb2016].
Google Groups discussion [retrieved 4Aug2016].
 CICM 2015:
GCH
implies AC, a Metamath Formalization (YouTube
video) [retrieved 19Jul2015]
(PDF slides)
(PPT)
(PDF paper) [retrieved
19Jul2015] by Mario
Carneiro.
Arithmetic in Metamath
Case Study: Bertrand's Postulate (CICM 2015) (YouTube
video) [retrieved 19Jul2015]
(PDF slides)
(PPT)
(PDF paper) [retrieved
19Jul2015] by Mario Carneiro.
 "Collapsible proof demo"
by Chris Capel (4Jan2011). (JavaScript is required.)
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 proofofconcept 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.

(In progress...)
AsteroidMeta metamath and mmj2 archived wiki
discussions (readonly; 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).
 grammarambiguity.txt 
a proof of the unambiguity of set.mm's grammar by Mario Carneiro
(28Apr2015)
 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
Principia Mathematica

Sean B. Palmer has created
some programs
[retrieved 6Oct2017] to verify these
independently and also to search for shorter proofs.
 Editor screenshots and syntax highlighting
for Metamath
 Robert Solovay's Metamath database source file
peano.mm (Peano arithmetic)
 Other Metamath database source files:
miu.mm (Hofstadter's MIUsystem),
bigunifier.mm
(William McCune's unification stress test),
demo0.mm
(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 ET16 scanner notes
(for NM's convenient reference; probably not interesting to others)
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)
 Sean B. Palmer has a
web page
[retrieved 6Oct2017] that runs the metamath program
in JavaScript. He writes,
"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).
Archived AsteroidMeta
wiki page [retrieved 3Aug2016] as of 2011.
 Milpgame
(28Feb2018) is a proof assistant and verifier, written in Java by
Filip Cernatescu.
 mmscala
[retrieved 13Jul2017]  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. See also
https://juliaobserver.com/packages/Metamath [retrived 9Jul2017].
 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). He also has written an
Introduction
to Metamath that summarizes the basics of the Metamath language,
which you may find useful.
 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).
 metamathada
(16Jul2017)  a simple Metamath proof checker [retrieved 15Aug2016]
(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
 mmpp is a proof editing environment for the
Metamath language, by Giovanni Mascellani. Still under development, the
GitHub project page
[retrieved 25Mar2018] has instructions for building it under Linux,
MacOS, and Windoows. See also the Google group
announcement [retrieved 25Mar2018].
 Metamath app  Bill Hale's app for Apple
desktop and iPad computers allows you to browse Metamath theorems and
their proofs. Do a search for "Metamath" to find it on Apple's app
store. It is free and has no ads or inapp purchases. For a demo of
this app, you can view the two YouTube videos
[retrieved 27Feb2018]. While its main display resembles the Metamath
web pages you are familiar with, a key feature is a "claim" screen to
view the breakdown of a single step of a proof (see the second video).
An online connection is not required since it stores set.mm locally.
(Bill Hale is also the author of mmide.)

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 11Apr2018]  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 12Apr2018)  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 by us at any time for any reason.

Cassie Williams requested the following resource links:
https://www.bestvalueschools.org/
https://www.bestvalueschools.org/financialaid/
https://www.bestvalueschools.org/bestresourcescollegestudentsdisabilities/
https://www.bestvalueschools.org/scholarship/
(Added 11Apr2018)
 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 20Sep2017)
 Branden Passwaters from OnlineCollegePlan requested a link to
the Top 100 Best Online Colleges. (Added 21Aug2017)
 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 6Jul2016)
 Francine Millar requested a link to
Most
Affordable Online Colleges for 2016
and wrote, "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 wrote, "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)
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:
http://www.reviews.com/studentinternshipplatforms/
http://www.reviews.com/studentinternshipplatforms/#What_Students_Should_Know_Before_Choosing_an_Internship_Platform
http://www.reviews.com/studentinternshipplatforms/#The_Best_Student_Internship_Platforms_of_2017
http://www.reviews.com/studentinternshipplatforms/#How_to_Avoid_Scams"
(Added 26Apr2016)
 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 29Mar2016)