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 us.
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
     
  • Older pages
  • Guest links
    		•  Other pages External links
    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.

    1. metamath-exe (current version), previously just called "metamath". This is 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. Metamath-knife - Metamath system written in Rust, a fork of metamath-rs (below).
    4. mm-lean4 [retrieved 7-May-2021] - a Metamath proof verifier written in Lean, by Mario Carneiro.
    5. zigmmverify [retrieved 5-May-2021] - a Metamath proof verifier written in Zig, by Marnix Klooster.
    6. gramm [retrieved 1-Oct-2018] - a Metamath proof verifier written in Antlr4/Java, by Naip Moro.
    7. Milpgame is a proof assistant and verifier, written in Java by Filip Cernatescu. For practice problems, see text linked at mpeuni/mmtheorems.html#problem1.
    8. mm-scala [retrieved 13-Jul-2017] - a Metamath proof verifier written in the Scala language as part of an ongoing Metamath -> MM import project
    9. Metamath.jl [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].
    10. 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."
    11. 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 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].
    12. MM Tool [retrieved 6-Sep-2015] - 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.
    13. Igor [retrieved 24-Sep-2015] - A proof assistant for Metamath, specialized for set.mm (written in a custom language by Drahflow; in progress)
    14. mmverify.py (27-Jan-2013) - the mmverify Metamath proof verifier (written in 350 lines of Python by Raph Levien)
    15. hmm.zip (3-Nov-2006) - the hmm Metamath proof verifier (written in 400 lines of Haskell by Marnix Klooster). External link: hmm [retrieved 3-Aug-2016]
    16. 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 [retrieved 3-Aug-2016]
    17. 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]
    18. checkmm.cpp (9-Dec-2010) - the checkmm Metamath proof verifier (written in C++ by Eric Schmidt)
    19. smetamath-rs - Metamath system engine [retrieved 3-Aug-2016] (written in Rust by Stefan O'Rear).
    20. metamath-ada (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.
    21. Metamatix is a verified implementation of a Metamath proof checker written using Coq.
    22. Sean B. Palmer has a web page [retrieved 6-Oct-2017] that runs the metamath (metamath-exe) C 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."
    Other tools for Metamath

    There are many other kinds of tools for Metamath. The metamath-exe and metamath-knife programs, previously mentioned, include a number of support functions that you may find useful.

    Here are some other tools for Metamath:

    1. 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.)
    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 set.mm. 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 11-Apr-2018] - 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 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 here). (Sadly, Alan Sare passed away on Mar. 23, 2019. The linked .zip file contains the last version that he provided.)
    7. 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].
    Metamath-related programs
    1. 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 post.
    2. gh_verify [retrieved 3-Aug-2016] - a verifier for the Ghilbert language (written in Python by Raph Levien)
    3. shullivan-0.05.zip (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). External link: http://home.alamedanet.net/~dan.krejsa/shullivan/shullivan.html [broken 3-Aug-2016].
    4. 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].
    5. 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.
    6. 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].
    7. 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: 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 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 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 ringcom.

    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 set.mm to achieve significant savings in proof sizes. See natded.pdf for slides and natded.mp3 for audio.

    Older pages
    Older pages:

    Hilbert Space Explorer - Extends ZFC set theory into Hilbert space, which is the foundation for quantum mechanics. Includes over 1,000 complete formal proofs.
    Hilbert Space Explorer

    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.
    Quantum Logic Explorer

    Metamath Solitaire - A Java applet that demonstrates simple proofs. Built-in axiom systems include ZFC; modal, intuitionistic, and quantum logics; and Tarski's plane geometry.
    Metamath Solitaire

    GIF and PNG Images for Math Symbols - A copyright-free collection of over 1,000 bit-mapped images for math symbols.
    GIF and PNG Images for Math Symbols

    Metamath Music Page - Strictly for fun. You can listen to what mathematical proofs "sound" like!
    Metamath Music Page
    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.

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