Week 10: Descendants, translations and comparisons

The languages that grew out of Metamath, the programs that carry proofs into and out of it, and one published comparison that sets it beside sixteen other provers.

10 May 2027

Metamath has descendants: languages that keep its small verifier and change something else. This lecture covers three, the programs that carry proofs into and out of Metamath, and one published comparison.

Metamath Zero. Its repository calls it “a language for writing specifications and proofs”, inspired by “Metamath and Lean, two proof languages at opposite ends of a spectrum” (digama0/mm0). It separates specification from proof, adds Metamath One, a language in which proofs are written and compiled, and states the goal: “to build a formally verified (in MM0) verifier for MM0, down to the hardware”. The 2019 paper, as its arXiv record describes it, “aims for simplicity of logic and implementation, without compromising on efficiency of verification”; the 2020 paper is indexed at its DOI without an abstract. The Trivial kernel checks MM0’s binary proof format.

Ghilbert and JHilbert. In Wiedijk’s survey, Megill describes Ghilbert as Raph Levien’s language “that has its roots in Metamath but guarantees the soundness of definitions” (PDF, p. 104). The Metamath site lists its verifier gh_verify, and JHilbert, “written in Java by Alexander Klauer” (other.html).

Russell. Its mdl program is “a compiler from a relativily high-level language for the representation of formal mathematics to the simple and robust for checking language Metamath” (dmitry-vlasov/russell); the Metamath site dates its download 10-Apr-2013 (other.html).

Translations. Carneiro’s 2014 paper, as its arXiv record describes it, converts proofs from OpenTheory, an exchange format for “the HOL family of proof languages”, into Metamath: first into hol.mm, then into set.mm. Outward, mm0-hs from-mm translates Metamath to MM0 (digama0/mm0); mm2dk translates Metamath to Dedukti. Two matching-logic projects, AML-Lean-to-Metamath and kore2mm, export into Metamath from Lean and from Kore.

Comparison. The Seventeen Provers of the World shows one proof, the irrationality of the square root of 2, in seventeen systems; Metamath’s entry (pp. 103–105) is by Megill: “It is a proof verifier, not an automated prover”. Five neighbours, each in its own words: Lean, “an open-source programming language and proof assistant”; the Rocq Prover, “formerly known as the Coq Proof Assistant”; Isabelle, “a generic proof assistant”; HOL Light, for “higher order logic”; and Mizar, which the Metamath home page says mimics published proofs, “whereas Metamath shows you every detail”.

Read#

• Metamath Zero README — what MM0 keeps from Metamath and what it changes.
• The Seventeen Provers of the World, pp. 103–105 — Metamath in its author’s words.