This page collects supplementary material related to Metamath. If you have
a topic you wish to add, contact us.
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 an interesting proof-of-concept demo showing some features
that are possible. Feel free to take over this project to
enhance it. Personally, I would prefer context-independent
icons that unambiguously indicate their function,
like the [+] for expand and [-] for collapse
in Windows Explorer. I would also prefer
to see the proof
sometimes I just want to see the whole proof at once without
having to open a dozen subtrees.
(Needs volunteer to reformat URLs...)
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 for Metamath
- 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
These are tools that can take the .mm database and verify that
it's correct (or not).
Some, such as Metamath-exe program (the
original C program) and mmj2, include functions to
help create proofs.
Note that some programs (like metamath-lamp) focus only on
helping create proofs and thus are put in a different list,
while other programs (like metamath-knife) are in this list but don't have
significant functions to help create proofs.
The 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-exe (current version),
previously just called "metamath".
This is 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.
- Metamath-knife - Metamath system written in Rust, a fork of metamath-rs (below).
[retrieved 7-May-2021] - a Metamath proof verifier written in Lean, by
[retrieved 5-May-2021] - a Metamath proof verifier written in Zig,
by Marnix Klooster.
[retrieved 1-Oct-2018] - a Metamath
proof verifier written in Antlr4/Java, by Naip Moro.
- Milpgame is a proof assistant
and verifier, written in Java by Filip Cernatescu. For practice
problems, see text linked at mpeuni/mmtheorems.html#problem1.
[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.
- Metamatix is a verified implementation of a Metamath proof checker
written using Coq.
- Sean B. Palmer has a
[retrieved 6-Oct-2017] that runs the metamath (metamath-exe) C 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."
Other tools for Metamath
There are many other kinds of tools for Metamath.
The metamath-exe and
programs, previously mentioned, include a number of support functions
that you may find useful.
Here are some other tools for Metamath:
- 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 in-app purchases. For a demo of
this app, you can view the two YouTube videos
[retrieved 27-Feb-2018]. 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 on-line connection is not required since it stores set.mm locally.
(Bill Hale is also the author of mmide.)
[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 11-Apr-2018] - 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].
(14-Sep-2016, updated 12-Apr-2018) - 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
(Sadly, Alan Sare passed away on Mar. 23, 2019. The linked .zip file contains
the last version that he provided.)
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].
XPuzzle [retrieved 1-Sep-2020] - a
puzzle with math formulas derived from the Metamath system (an Android
App by Filip Cernatescu). At the bottom of the web page is a link to
the Google Play Store. See also this Google Group
- 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].
- Raph Levien has developed a related language called Ghilbert
that strives to improve upon Metamath by guaranteeing the soundness of
definitions and providing features useful for collaborative work.
- 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.
Hilbert Space Explorer -
Extends ZFC set theory into Hilbert space,
which is the foundation for quantum mechanics. Includes over
1,000 complete formal proofs.
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.
Metamath Solitaire - A Java
that demonstrates simple proofs.
Built-in axiom systems
include ZFC; modal, intuitionistic, and quantum logics; and Tarski's
Metamath Music Page - Strictly
for fun. You can listen
to what mathematical proofs "sound" like!
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.
- Barry Franklin from Health Care Degree writes, "High-quality
education comes at a price. It's common for students to take large
amounts of debt to fulfill their higher education dreams and it can take
decades to pay off student loans. With that in mind, the team at
HealthCareDegree.com is highlighting a great guide titled Issues
in Healthcare Career Scholarship Guide (2021-2022). We also have
created more Blog
and FAQ content that
you might find useful as well.
- Marc from PCWDLD writes, "My colleague's Cygwin 'cheat sheet' -
https://www.pcwdld.com/cygwin-cheat-sheet - is a quick reference to
Cygwin that I think could be useful. It's not a cheat sheet in the
traditional sense as it's more about helping someone to get started with
Cygwin then providing some shortcuts to make life easier."
- Hicham Benali requested a link to
hand-picked, regularly updated (listed by deadline) disability
scholarships that you can apply for, to reduce your fees."
- Sandra writes, "Recently, I have conducted research and collected a
list of financial aid and scholarships for students with various special
needs, you can find it here:
All the provided information is verified and up-to-date."
- Andy Kearns writes, "I work on the Consumer Education team at
LendEDU.... We have a guide on our site titled Guide to Paying for College
for People With Disabilities and I believe it can be a useful addition
to your page. Here's the full guide:
We hope college students with disabilities can use this resource to find
various forms of financial aid available to them including scholarships,
grants, support programs, and more."
- Sujin with study.com writes, "The team at Study.com recently developed
a comprehensive college guide for students with disabilities. Our goal
is to inform students about critical information regarding their college
education to help set them up for success. The College
Guide for Students with Disabilities offers in-depth details in
several areas, including:
- Legal rights of students with disabilities
- Services colleges can or need to make available
- Required accommodations for students
- Technologies and helpful apps for students"
- Joanne Davis writes, "Recently, I have conducted
research and collected a list of technologies for people with
It is up to date and contains only verified and useful information."
- Nicole Cowart with Essayontime writes, "Recently, we have conducted
research and gathered a list of financial aid and scholarships for
students with special needs. You can find it here:
All the provided information is verified and up-to-date."
- Cheri Shallenberger with College Explorer writes, "We focus extensively
on helping students research higher education and labor trends in the
online higher education sectors. We recently updated our College
Education Guides to help job seekers, professionals, and students
understand the changing landscapes of these programs and their impact on
careers and employment. You can view the guides here:
We also recently updated our mental health education pages to help job
seekers and students understand the changing landscapes of these programs
and their impact on careers and employment for the future:
Beckie Stone requested the following resource links:
Cassie Williams requested the following resource links:
- 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)