Research map / Large language models / Agents, code and math
Retrieval-augmented formal theorem proving
Prove theorems with language models using retrieval, hammers, and subgoal demonstrations.
62 accepted papers at ICML, NeurIPS, ICLR, CVPR and AAAI (2019–2026) · an approach in Agents, code and math, keyword cluster “theorem · proof · proving”
State History Tried Checklist Preprints Who Export
Where it stands
Not enough benchmark data Fewer than four papers report the same benchmark, so there is no record to follow.
18 papers in 2023–24 and 34 in 2025–26 (at ICML, NeurIPS, ICLR, CVPR and AAAI); its share of the topic shrank, from 5.0% to 2.7%.
How this is decided
A benchmark is tracked when at least four papers of this approach report their own method on the same dataset and metric in at least two different years. Its record is the best number reported up to 2024 compared with the best reported in 2025–26: still improving means at least 1% better, flat means at most 0.2% better with at least two papers from 2025–26 trying. Numbers on a different scale from the rest (a fraction among percentages) and far outliers are left out. Results come from different papers with different setups, so they are signals, not head-to-head comparisons. The share of papers is counted at ICML, NeurIPS, ICLR, CVPR and AAAI.
How it got here
Most cited paper of each year
- 2019 · HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving (ICML 2019 · 65 citations)
- 2020 · Learning to Prove Theorems by Learning to Generate Theorems (NeurIPS 2020 · 17 citations)
- 2021 · NaturalProofs: Mathematical Theorem Proving in Natural Language (NeurIPS 2021 · 13 citations)
- 2022 · miniF2F: a cross-system benchmark for formal Olympiad-level mathematics (ICLR 2022 · 25 citations)
- 2023 · LeanDojo: Theorem Proving with Retrieval-Augmented Language Models (NeurIPS 2023 · 39 citations)
- 2024 · Llemma: An Open Language Model for Mathematics (ICLR 2024 · 15 citations)
- 2025 · VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification (NeurIPS 2025 · 2 citations)
- 2026 · MathlibLemma: Folklore Lemma Generation and Benchmark for Formal Mathematics (ICML 2026 · 0 citations)
Earliest papers here
- HOList: An Environment for Machine Learning of Higher Order Logic Theorem Proving (ICML 2019 · 65 citations)
- GamePad: A Learning Environment for Theorem Proving (ICLR 2019 · 56 citations)
- Learning to Prove Theorems via Interacting with Proof Assistants (ICML 2019 · 21 citations)
What has been tried
36 papers here report 344 measured changes (a component added, removed or swapped, compared with a baseline): helped 74%, no clear effect 6%, hurt 19%, mixed 1%. Papers mostly publish changes that helped, so "helped" is over-represented.
Ablations in recent papers
| What was changed | Measured on | Result | Effect | Paper |
|---|---|---|---|---|
| use one-step theorem prediction instead of theorem traversal | Geometry3K, KB1 · accuracy | 77.0 -> 79.8 | Helped | E-GPS: Explainable Geometry Problem Solving via Top-Down Solver and Bottom-Up Generator (CVPR 2024 · 10 citations) |
| Add the growing skill library, including the evolver | miniF2F-valid · success rate | 47.1% -> 50.4% | Helped | LEGO-Prover: Neural Theorem Proving with Growing Libraries (ICLR 2024 · 9 citations) |
| Remove the Rerank stage | PISA, budget 800 · proof success rate (%) | 56.3% -> 54.2% | Hurt | Magnushammer: A Transformer-Based Approach to Premise Selection (ICLR 2024 · 9 citations) |
| add retrieval to ReProver | PutnamBench Lean 4 · success rate | 0/640 -> 0/640 | No clear effect | PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competition (NeurIPS 2024 · 5 citations) |
| Add reasoning traces rather than use instruction-only training examples | VeriThoughts · Pass@1 | 49.0% -> 75.5% (Diff. 26.5%) | Helped | VeriThoughts: Enabling Automated Verilog Code Generation using Reasoning and Formal Verification (NeurIPS 2025 · 2 citations) |
| Apply expert iteration without CoT, using (state, tactic) pairs only | miniF2F-test · Pass@32 | 41.3% -> 43.0% | Helped | Lean-STaR: Learning to Interleave Thinking and Proving (ICLR 2025 · 2 citations) |
| replace beam-search decoding with sampling | miniF2F-valid · pass@1 | 39.3% -> 30.3% | Hurt | Proving Theorems Recursively (NeurIPS 2024 · 2 citations) |
| use transition-model embeddings instead of tactic-reconstruction autoencoder embeddings | miniF2F-valid Pass@1, K=8 · Pass@1 | 23.0 -> 25.0 | Helped | 3D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processes (NeurIPS 2025 · 1 citation) |
| Add value curriculum fine-tuning to the pretrained value network | MO-INT-20 · problems solved | 7 -> 10 | Helped | Proving Olympiad Algebraic Inequalities without Human Demonstrations (NeurIPS 2024 · 1 citation) |
| Add ProofAug to the DSP baseline | miniF2F-test (Isabelle) · pass rate | 28.7% -> 36.5% (+7.8%) | Helped | ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysis (ICML 2025 · 0 citations) |
| add proofs of generated conjectures to final retraining | miniF2F-test, pass@128 · pass rate | 58.3% ± 0.7% -> 61.2% ± 0.6% | Helped | STP: Self-play LLM Theorem Provers with Iterative Conjecturing and Proving (ICML 2025 · 0 citations) |
| Scale model size from 7B to 671B | Ineq-Comp Type I · pass@32 accuracy | 46.97 -> 68.33 | Helped | Ineq-Comp: Benchmarking Human-Intuitive Compositional Reasoning in Automated Theorem Proving of Inequalities (NeurIPS 2025 · 0 citations) |
What reviewers will expect
Datasets and baselines named in the 15 papers of this approach from 2025–2026 that have a full-text summary. Leaving out the common ones is a frequent review question.
Datasets
- miniF2F · 6 of 15 papers
- LeanWorkbook · 2 of 15 papers
- Mathlib4 · 2 of 15 papers
- miniF2F-valid · 2 of 15 papers
- miniF2F-test · 2 of 15 papers
- PutnamBench · 2 of 15 papers
- ProofNet · 2 of 15 papers
Baselines
- DeepSeek-Prover-V1.5-RL · 4 of 15 papers
- ReProver · 3 of 15 papers
- Goedel-Prover-SFT · 3 of 15 papers
- DSP · 2 of 15 papers
- RMaxTS · 2 of 15 papers
- HTPS · 2 of 15 papers
- InternLM2.5-StepProver · 2 of 15 papers
- STP · 2 of 15 papers
Recent preprints
Loading recent arXiv preprints…
Who publishes on it
Institutions on the most papers of this approach since 2023 (of 52 papers; from OpenAlex and the papers' affiliations).
- Cornell University · 4 papers
- Huawei · 4 papers
- The Chinese University of Hong Kong · 4 papers
- Stanford University · 3 papers
- University of Edinburgh · 3 papers
- Tsinghua University · 3 papers
- King's College London · 2 papers
- Google DeepMind · 2 papers
- University of Cambridge · 2 papers
- Meta · 2 papers
Use it
Download BibTeX of 34 key papersOpen the topic in the interactive map
Get alerts. Describe your idea in scime atlas and save it (free scime account): you get a weekly email when new preprints land close to it.
Related approaches
Same keyword cluster
- Formal verification and proof data (25 papers)
Elsewhere in the topic
- Mathematical and structural reasoning benchmarks (304 papers)
- Agent instruction-following benchmarks (176 papers)
- Inductive and abstract reasoning evaluation (158 papers)
- Long-horizon LLM agents (155 papers)
- LLMs for optimization and heuristics (147 papers)
- Software engineering agents (140 papers)
- LLMs for scientific discovery (100 papers)
- Code generation benchmarks (96 papers)
Benchmark numbers, ablations and baseline numbers are extracted by AI from each paper's full text and can be wrong; the paper is the authority. Data: results index of 2026-11-02, citation counts from OpenAlex (2026-10-09).