Generative Language Modeling for Automated Theorem Proving

The founding paper of LLM-based theorem proving — a methods/system paper from OpenAI (Polu & Sutskever, Sep 2020) that jiang2026 correctly names as where “the lineage begins.” Its motivating diagnosis still defines the field: classical ATP’s limiting weakness is generating original mathematical terms (the creative substitutions unification can’t derive), and autoregressive generation addresses exactly that. The headline result is cultural as much as technical: 23 shortened proofs generated by GPT-f were accepted into Metamath’s set.mm — the first time a deep-learning system’s proofs were adopted by a formal mathematics community, verified not just by a kernel but by human maintainers merging PRs.

The system

Decoder-only transformers (160m–1.5b params; best results at 774m labeled “700m”) trained on a proofstep objective: literally GOAL <goal> PROOFSTEP <tactic> as conditional language modeling over ~3M proof steps from set.mm’s ~38k theorems. Proof search is best-first by cumulative logprob (e=32 sampled tactics per expansion, d=128–256 expansions, a=4–32 attempts), against a purpose-built Python Metamath kernel — the tight generator/verifier coupling every successor inherited. Metamath was chosen for machine-friendliness (context-free proof steps, trivial verification) at a known cost: a de Bruijn factor of ~10–20 versus ~1–3 for Coq/HOL/Lean, meaning very long low-level proofs. Final score: 56.22% of the held-out test set, versus 21.16% for the prior state of the art (MetaGen-IL’s three small GRUs — the comparison is generous to no one, but the gap made the paradigm case).

Four findings that became the field’s playbook

1. Pretraining transfers into formal reasoning, and math-adjacent beats generic. 700m from scratch 31.6% → CommonCrawl 39.6% → WebMath (GitHub + arXiv math + Math StackExchange) 42.6%.
2. Scale helps despite tiny formal corpora — monotone 160m→700m, with an honest anomaly flagged: 1.5b plateaus, an early sighting of formal-data saturation.
3. Expert iteration with the verifier as ground truth. The value function is an outcome objective — append OUTCOME P|N and read the token probability, no value head — trained on the prover’s own search trees, then used to guide subsequent search: 42.6% → 47.2% over two iterations, with the paper explicitly proposing “keep training on proofs generated by the prover.” This is the loop DeepSeek-Prover’s RLPAF and AlphaProof’s self-play later ran at scale.
4. Synthetic proof generation (n-digit arithmetic, ring equalities) with a controlled sample-complexity study: ~100 synthetic proofs suffice to lift a task from ~10% to ~80–90% — evidence that new capabilities are learnable at manual-formalization cost.

One buried observation aged particularly well: overfitting doesn’t much hurt static evaluation but destroys iterative training — an overconfident model collapses exploration in its own data generation. That is the feedback-quality failure mode zhang2025 later formalized for context evolution, observed here in weight space in 2020.

Assessment

• Durable: the proofstep objective as the recipe (modern provers still train on serialized goal→tactic text); verifier-coupled search; expert iteration; pretraining transfer; and the adoption bar — a contribution counts when the community merges it, the same verification-before-persistence standard wang2023 later applied to skills.
• Era-bound: Metamath itself (the field moved to Lean for exactly the expressiveness reasons §3 lists), the parameter counts, and the search economics (~1k V100-hours per evaluation).
• Caveats: never peer-reviewed, which given its influence is a comment on venue lag, not the work.
• In this library: reading it after jiang2026 is an exercise in recognition — pretraining data curation, RL from verifier feedback, synthetic data, iterative self-improvement: the 2026 taxonomy’s whole training-strategies axis is present here in miniature. And the arc from this paper’s 23 shortened Metamath proofs to openai2026‘s claimed frontier results is the same lab, six years apart — the modest, humanly verified beginning of the trajectory whose loudest claim the library now also holds.