aleph-null logo Other Metamath-Related Topics  
Mirrors  >  Home  >  Other

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
  • Other tools for Metamath
  • Metamath-related programs
  • Mathematica program to generate arithmetic proof steps
  • Study of complex number axiomatization
  • Natural deduction in Metamath
  • Guest links
  • Other pages
  • The Metamath 100 list
  • CICM 2016: Prime Number Theorem (PDF slides) (PPT) by Mario Carneiro, with an informal exposition of the related Dirichlet's theorem [retrieved 4-Aug-2016]. Models for Metamath (PDF slides) (PPT) (PDF paper) by Mario Carneiro; the paper is also available at [retrieved 16-Feb-2016]. Google Groups discussion [retrieved 4-Aug-2016].
  • CICM 2015: GCH implies AC, a Metamath Formalization (YouTube video) [retrieved 19-Jul-2015] (PDF slides) (PPT) (PDF paper) [retrieved 19-Jul-2015] by Mario Carneiro. Arithmetic in Metamath Case Study: Bertrand's Postulate (CICM 2015) (YouTube video) [retrieved 19-Jul-2015] (PDF slides) (PPT) (PDF paper) [retrieved 19-Jul-2015] by Mario Carneiro.
  • "Collapsible proof demo" by Chris Capel (4-Jan-2011). (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 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.
  • (In progress...) AsteroidMeta metamath and mmj2 archived wiki discussions (read-only; partial recovery to Nov. 2008). Missing pages are sometimes on e.g. page for metamath (but LaTeX math image files may be missing after 2013 or so).
  • grammar-ambiguity.txt - a proof of the unambiguity of's grammar by Mario Carneiro (28-Apr-2015)
  • 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
  • Editor screenshots and syntax highlighting for Metamath
  • Robert Solovay's Metamath database source file (Peano arithmetic)
  • Other Metamath database source files: (Hofstadter's MIU-system), (William McCune's unification stress test), (toy formal system)
  • Current web usage statistics ( 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)
  • 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.

    1. metamath (current version) - the original Metamath proof verifier and proof assistant (written in C by Norman Megill)
    2. mmj2 proof assistant and verifier (written in Java by Mel O'Cat; enhanced and maintained by Mario Carneiro). Archived AsteroidMeta wiki page [retrieved 3-Aug-2016] as of 2011.
    3. mm-scala [retrieved 14-Aug-2016] - a Metamath proof verifier written in the Scala language as part of an ongoing Metamath -> MM import project
    4. Metamath.jl [retrieved 12-Jun-2016] - a Metamath proof verifier written in the Julia language, by Dan Getz.
    5. 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 anymore), but it will catch all the important errors. It also works with both normal and compressed proofs."
    6. smm [retrieved 6-Sep-2015] - the smm, smm2, smm3 Metamath proof verifiers (written in JavaScript by Stefan O'Rear) with a long-term goal of providing another proof assistant. By using multiple threads, smm3 verifies 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].
    7. MM Tool [retrieved 6-Sep-2015] - a Metamath proof verifier and editor that runs in a browser (written in JavaScript by Ivan Kuckir)
    8. Igor [retrieved 24-Sep-2015] - A proof assistant for Metamath, specialized for (written in a custom language by Drahflow; in progress)
    9. (27-Jan-2013) - the mmverify Metamath proof verifier (written in 350 lines of Python by Raph Levien)
    10. (3-Nov-2006) - the hmm Metamath proof verifier (written in 400 lines of Haskell by Marnix Klooster). External link: hmm [retrieved 3-Aug-2016]
    11. verify.lua (21-Oct-2006) - a Metamath proof verifier (written in 380 lines of Lua by Martin Kiselkov; needs 40 min to verify, but provides an interesting example for learning Lua). External link: verify.lua [retrieved 3-Aug-2016]
    12. Verifier.cs (29-Oct-2010) - a Metamath proof verifier (written in 550 lines of C# by Chris Capel). External link: verifier.cs [retrieved 3-Aug-2016]
    13. checkmm.cpp (9-Dec-2010) - the checkmm Metamath proof verifier (written in C++ by Eric Schmidt)
    14. smetamath-rs - Metamath system engine [retrieved 3-Aug-2016] (written in Rust by Stefan O'Rear).

    Other tools for Metamath
    1. 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 theory file. (Note: The software is closed source, and I cannot vouch for the integrity of the binaries.)
    2. Holophrasm [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 Other links: paper [retrieved 22-Aug-2016], working release [retrieved 22-Aug-2016].
    3. metamath-test [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].
    4. EMetamath [retrieved 3-Aug-2016] - Metamath plugin for Eclipse IDE, with mmj2 inside (written in Java by Thierry Arnoux). Google Groups discussion [retrieved 10-Jul-2016].
    5. Metamath 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].
    6. completeusersproof (14-Sep-2016, updated 18-Feb-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 edu.
    7. (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].

    Metamath-related programs
    1. gh_verify [retrieved 3-Aug-2016] - a verifier for the Ghilbert language (written in Python by Raph Levien)
    2. (14-Jan-2007) - a verifier for the Ghilbert language (written in C by Dan Krejsa; loads and verifies the translated 2008 in 500 ms). External link: [broken 3-Aug-2016].
    3. (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].
    4. (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].
    5. mdl-0.8.7-72.tar.gz (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: [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 metamath program).

    Study of complex number axiomatization

    In June 2012, Eric Schmidt discovered that two of our Axioms for Complex Numbers, namely ax-addcom (now addcom) and ax-0id (now addid1), were redundant. His results are described in schmidt-cnaxioms.pdf (LaTeX source schmidt-cnaxioms.tex), which also includes independence results for the remaining axioms. 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 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 12-Jul-2015]. It describes the natural deduction emulation method (prefixing hypotheses and theorems with "ph ->") that we now commonly use in 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.

      This page was last updated on 18-Feb-2017.
    Your comments are welcome: Norman Megill nm at alum dot mit dot edu
    Copyright terms: Public domain
    W3C validator   Mobile check