AI4Math ChronicleAI4Math 大事记

Holophrasm builds a neural end-to-end theorem prover for Metamath

Holophrasm parses Metamath statements into tree structures, learns neural models for proof-step generation and proof-state evaluation, and combines them with search over candidate proof trees.

What happened?

Daniel Whalen introduced Holophrasm, a neural automated theorem prover for Metamath that explored partial proof trees with a neural-network-augmented bandit algorithm and used a sequence-to-sequence model to enumerate proof actions. The paper reported proving about 14% of its held-out test theorems from Metamath's `set.mm` corpus.

Holophrasm parses Metamath statements into tree structures, learns neural models for proof-step generation and proof-state evaluation, and combines them with search over candidate proof trees. The public release includes model-training and proof-search code, saved proof outputs, and instructions for replaying generated proofs through Metamath's verifier.

Why it matters

The project demonstrated a pre-Transformer route to neural proof generation in which learned models actively construct formal proof steps rather than only rank premises. Its Metamath data-processing and prover structure were reused by later work, including MetaGen, making it a durable part of the lineage of neural formal theorem proving.

Significance rationale: Holophrasm was an important early neural theorem prover that moved beyond premise scoring to search over complete formal proof trees in Metamath. It combined learned proof-step generation, neural evaluation and bandit-style search in one system, creating a direct historical precursor to later Metamath neural provers and synthetic-data systems such as MetaGen.

Historical context

Earlier developments

—

Later developments
Related milestones

—

Primary evidence

Evidence & status at a glance

Significance
H2 · Field milestone
Verification
Paper released
Evidence level
E3 · Inspectable artifact
AI role
Autonomous primary role
Formal assurance
Machine-checked

How should these labels be read? →

Contribution & verification

Mathematical novelty
Tooling only
Interface
Formal, Symbolic
AI contribution
Learned neural models proposed proof actions and evaluated proof states while the search procedure assembled complete formal proofs; successful outputs could then be checked by Metamath without human step-by-step proof construction.
Human contribution
The researcher designed the Metamath parser, neural models, search algorithm, training pipeline and evaluation protocol, and packaged the generated proofs for replay and verification.
Verification
Paper released · E3 · Inspectable artifact · Machine-checked
Last reviewed
2026-09-15

Technical details

Systems
holophrasm, metamath
Organizations
—
Problems
metamath-theorem-proving, automated-theorem-proving
Methods
neural-theorem-proving, sequence-to-sequence-generation, bandit-search, proof-tree-search, proof-step-generation

Sources & artifacts

Verification history

  • 2016-08-08 · Paper released · E2 · Research record

    The arXiv research record establishes Holophrasm, its neural proof-search architecture and the reported Metamath evaluation. Machine checking refers to formal proofs that can be replayed through Metamath and does not imply independent reproduction of the paper's aggregate success rate.

  • 2026-09-15 · Paper released · E3 · Inspectable artifact

    The public Holophrasm repository exposes training and search code, saved proof outputs and explicit Metamath verification instructions. E3 denotes inspectable artifacts rather than an independent rerun of the complete experiment.

Corrections

No corrections recorded.