Week 9: Formalisation in practice

What large Metamath proofs cost, from the ones that exist: GCH implies AC, the prime number theorem, Bertrand's postulate, a proof done on video, legibility research, and the 100 theorems scoreboard.

3 May 2027

Three of the largest formalisations in set.mm are by one author, and the record of each says what it cost.

GCH implies AC. Mario Carneiro presented “GCH implies AC, a Metamath Formalization” at CICM 2015; metamath.org’s other topics page links the video, slides and paper. The paper’s abstract, as OpenAlex records it, describes Specker’s “local” version of the claim “with particular attention to some extra complications which were glossed over in the original informal proof.” That is the recurring lesson: an informal proof glosses, and a formal one cannot.

The prime number theorem. The Metamath 100 page, at set.mm commit 2c1dffe, dates pnt to 2016-06-01 and Dirichlet’s theorem dirith to 2016-05-12, both by Mario Carneiro. The CICM 2016 talk and the paper cover both: Selberg’s elementary proof of the prime number theorem, “within the proof system Metamath.”

Bertrand’s postulate. bpos is in set.mm, by Mario Carneiro, 2014-03-15, per the same page, which also records the iset.mm version, added by Jim Kingdon on 2026-09-10: last week’s lab at full scale. A CICM 2015 paper, “Arithmetic in Metamath, Case Study: Bertrand’s Postulate”, is listed on metamath.org beside the GCH talk.

A proof on camera. “Formalizing Geometric Proof Schwabhäuser 4.6 in the Metamath Proof Explorer” (19-Jul-2020) is among David A. Wheeler’s videos listed on metamath.org.

Legibility as a research question. Lindsay, Kaliszyk and Rizkallah (2026) argue, in the abstract as OpenAlex records it, that Metamath’s “verification architecture prioritises algorithmic efficiency over human readability,” and that reordering inferences can cut a reader’s working memory load without changing proof size. Oliveira and Pimentel (2021) propose adapting the level of detail at which a proof is shown, using Metamath’s step-level structure.

The scoreboard. Formalizing 100 Theorems (last modified 2026-09-06) puts Metamath at 74 of the hundred, behind HOL Light (95), Isabelle (92), Lean (83) and Rocq (80). Metamath 100, at commit 2c1dffe, says “Currently there are 75 proofs proven by Metamath from this list of 100,” with its comparison dated 2026-04-28. Its to-do list includes Gödel’s incompleteness theorem and Fermat’s last theorem.

Read#

• Metamath 100: every proof on the list with its label, author and date; skim for how big proofs are named.
• Formalization of the prime number theorem and Dirichlet’s theorem: the account of the largest of the three.
• Optimising Metamath Proofs for Human Working Memory: why the order of steps matters to a reader, which Wednesday’s plan is about.