Primary evidence
- Generative language modeling for automated theorem provingS2 · Official institutional · Official announcement · 2020-09-07
- Generative Language Modeling for Automated Theorem ProvingS1 · Primary research · Paper · 2020-09-07
GPT-f brings generative language modeling to formal theorem proving
OpenAI researchers Stanislas Polu and Ilya Sutskever trained generative models over formal mathematical text and integrated them into proof search for the Metamath language.
What happened?
GPT-f used a generative transformer model to search for proofs in Metamath and found new shorter proofs that were accepted into the main Metamath library.
OpenAI researchers Stanislas Polu and Ilya Sutskever trained generative models over formal mathematical text and integrated them into proof search for the Metamath language. The work framed theorem proving as sequence generation and showed that learned generation could contribute usable proof artifacts to an established formal library.
Why it matters
The result is a useful starting point for the later LLM-plus-proof-assistant line of AI4Math, where language models propose proof actions and formal systems provide exact feedback.
Significance rationale: GPT-f was an early demonstration that transformer language models could generate formal proof steps rather than only score or classify them, and its authors reported new shorter proofs accepted into the Metamath library.
Historical context
Earlier developments
—
Later developments
- miniF2F establishes a cross-system benchmark for formal Olympiad mathematics
- LeanDojo opens a reproducible environment for LLM theorem proving in Lean
- COPRA turns a general LLM into a stateful formal proof-search agent
- DeepSeek-Prover-V1.5 combines proof-assistant feedback, reinforcement learning and tree search
Related milestones
—
Evidence & status at a glance
- Significance
- H2 · Field milestone
- Verification
- Paper released
- Evidence level
- E2 · Research record
- AI role
- AI primary, human verified
- Formal assurance
- Machine-checked
Contribution & verification
- Mathematical novelty
- New proof
- Interface
- Formal, Symbolic
- AI contribution
- The model generated candidate proof steps and proof searches; Metamath mechanically checked resulting proofs before they could be accepted.
- Human contribution
- Researchers designed the model and search procedure, selected the formal corpus and evaluation, and the Metamath community maintained the target library and reviewed contributions.
- Verification
- Paper released · E2 · Research record · Machine-checked
- Last reviewed
- 2026-09-11
Technical details
- Systems
- gpt-f, metamath
- Organizations
- openai, metamath-community
- Problems
- —
- Methods
- transformer-language-modeling, formal-theorem-proving, proof-search
Sources & artifacts
- Generative language modeling for automated theorem provingS2 · Official institutional · Official announcement · accessed 2026-09-10
- Generative Language Modeling for Automated Theorem ProvingS1 · Primary research · Paper · accessed 2026-09-10
Verification history
- 2020-09-07 · Paper released · E2 · Research record
OpenAI and the arXiv paper reported the Metamath prover and the adoption of generated shorter proofs into the library.
Corrections
No corrections recorded.