Week 11: Machine learning on Metamath

The papers that trained programs to find Metamath proofs, in order from 2016 to 2025, the datasets and tools built for them, and a name collision to know about.

17 May 2027

Since 2016 a line of papers has used set.mm to train and test programs that search for proofs. This lecture takes them in order, each as its own abstract describes it. A held-out set, below, is the group of theorems kept back from training.

• Holophrasm (2016). Daniel Whalen’s system, as its record describes it, explores partial proof trees with “a neural-network-augmented bandit algorithm” and “proves 14% of its test theorems from Metamath’s set.mm module”.
• GPT-f (2020). Polu and Sutskever present “an automated prover and proof assistant, GPT-f, for the Metamath formalization language” (record). It “found new short proofs that were accepted into the main Metamath library”, which the abstract calls “the first time a deep-learning based system has contributed proofs that were adopted by a formal mathematics community”. Which proofs is not stated there.
• MetaGen (2020). Wang and Deng train “a neural generator that automatically synthesizes theorems and proofs for the purpose of training a theorem prover”, with experiments in Metamath (record).
• HyperTree Proof Search (2022). Lample and colleagues describe a search “inspired by the recent success of AlphaZero”; their record reports 65.4% of a held-out set of Metamath theorems against “56.5% by GPT-f”, rising to 82.6% with online training (record).
• REFACTOR (2024). Zhou and colleagues train a network to extract reusable theorems from proofs; applied “to the existing Metamath library, REFACTOR extracted 16 new theorems” (record).
• Grammar-compressed proof terms (2025). Wernhard and Zombori take Metamath as their “source of human-structured proofs” and treat a knowledge base as “a grammar that compresses a set of gigantic proof trees” (record).

Three repositories serve this work. mm-atp-benchmark is, per its GitHub listing, a “Metamath ATP Benchmark created from set.mm”; synthetic-mm is “a synthetic data framework for Metamath”; Compass calls itself “A high performance metamath ITP to train for neural theorem proving” and, in the next line, “Project abandoned in favour of LeanDojo and MM0”.

One name to know: “MetaMath: Bootstrap Your Own Mathematical Questions for Large Language Models” (2023) and its dataset MetaMathQA. Its record describes a language model fine-tuned on rewritten mathematical questions and scored on the GSM8K and MATH benchmarks; nothing in that record concerns the Metamath language.

Read#

• GPT-f abstract — the claim that machine-found proofs entered set.mm.
• HyperTree Proof Search abstract — the numbers later work measures against.