mlsanityData to 7 Oct 2026

Generative Language Modeling for Automated Theorem Proving

arXiv 2009.03393 ↗First posted 7 Sep 2020cs.LG cs.AI cs.CLcited by 379

On the map: LLM reasoning → Mathematical reasoning

Abstract (arXiv)

We explore the application of transformer-based language models to automated theorem proving. This work is motivated by the possibility that a major limitation of automated theorem provers compared to humans -- the generation of original mathematical terms -- might be addressable via generation from language models. We present an automated prover and proof assistant, GPT-f, for the Metamath formalization language, and analyze its performance. GPT-f found new short proofs that were accepted into the main Metamath library, which is to our knowledge, the first time a deep-learning based system has contributed proofs that were adopted by a formal mathematics community.

Key facts. Cited by 379 papers in the map (data through 7 Oct 2026). Placed in Mathematical reasoning, one of 17 directions in LLM reasoning. Builds on 3 of its 47 references that are in the map. First posted on arXiv 7 Sep 2020.

Builds on

3 of 47 references.

References · 3

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2019Solving Rubik's Cube with a Robot Handcited by 699
  3. 2017Thinking Fast and Slow with Deep Learning and Tree Searchcited by 245

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 27; 2022: 40; 2023: 44; 2024: 76; 2025: 106; 2026: 86.

379 papers.

Sort:

By area:

  1. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  2. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  3. 2025DAPO: An Open-Source LLM Reinforcement Learning System at Scalecited by 2,678
  4. 2023A Survey of Large Language Modelscited by 2,537
  5. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  6. 2022STaR: Bootstrapping Reasoning With Reasoningcited by 895
  7. 2021Measuring Coding Challenge Competence With APPScited by 879
  8. 2022Solving math word problems with process- and outcome-based feedbackcited by 871
  9. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  10. 2023Llemma: An Open Language Model For Mathematicscited by 385
  11. 2025Towards Reasoning Era: A Survey of Long Chain-of-Thought for Reasoning Large Language Modelscited by 381
  12. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
38 more
  1. 2024Quiet-STaR: Language Models Can Teach Themselves to Think Before Speakingcited by 292
  2. 2024Inference Scaling Laws: An Empirical Analysis of Compute-Optimal Inference for Problem-Solving with Language Modelscited by 282
  3. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  4. 2023ToRA: A Tool-Integrated Reasoning Agent for Mathematical Problem Solvingcited by 276
  5. 2025DeepSeek-Prover-V2: Advancing Formal Mathematical Reasoning via Reinforcement Learning for Subgoal Decompositioncited by 270
  6. 2022Transformers Learn Shortcuts to Automatacited by 260
  7. 2022Autoformalization with Large Language Modelscited by 252
  8. 2024DeepSeek-Prover: Advancing Theorem Proving in LLMs through Large-Scale Synthetic Datacited by 225
  9. 2022Memorizing Transformerscited by 219
  10. 2022End-to-end symbolic regression with transformerscited by 195
  11. 2025The Landscape of Agentic Reinforcement Learning for LLMs: A Surveycited by 195
  12. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  13. 2024DeepSeek-Prover-V1.5: Harnessing Proof Assistant Feedback for Reinforcement Learning and Monte-Carlo Tree Searchcited by 189
  14. 2021Neural Symbolic Regression that Scalescited by 185
  15. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  16. 2022A Review on Language Models as Knowledge Basescited by 156
  17. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  18. 2023OpenWebMath: An Open Dataset of High-Quality Mathematical Web Textcited by 151
  19. 2021Explaining Answers with Entailment Treescited by 148
  20. 2021Inductive Biases and Variable Creation in Self-Attention Mechanismscited by 144
  21. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  22. 2022mGPT: Few-Shot Learners Go Multilingualcited by 141
  23. 2021Investigating the Limitations of Transformers with Simple Arithmetic Taskscited by 136
  24. 2024From Decoding to Meta-Generation: Inference-time Algorithms for Large Language Modelscited by 136
  25. 2023Focused Transformer: Contrastive Training for Context Scalingcited by 133
  26. 2024Rho-1: Not All Tokens Are What You Needcited by 132
  27. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  28. 2023How well do Large Language Models perform in Arithmetic tasks?cited by 130
  29. 2023Self-Taught Optimizer (STOP): Recursively Self-Improving Code Generationcited by 128
  30. 2025Goedel-Prover: A Frontier Model for Open-Source Automated Theorem Provingcited by 126
  31. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  32. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  33. 2022Teaching Algorithmic Reasoning via In-context Learningcited by 111
  34. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  35. 2021Case-based Reasoning for Natural Language Queries over Knowledge Basescited by 107
  36. 2022Language Model Cascadescited by 104
  37. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  38. 2024Easy-to-Hard Generalization: Scalable Alignment Beyond Human Supervisioncited by 95

50 most cited of 379 All 379 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2025Autoformalization in the Era of Large Language Models: A Survey
  2. 2025Theorem Prover as a Judge for Synthetic Data Generation
  3. 2023math-PVS: A Large Language Model Framework to Map Scientific Publications to PVS Theories
  4. 2025Mathesis: Towards Formal Theorem Proving from Natural Languages
  5. 2025IndiMathBench: Autoformalizing Mathematical Reasoning Problems with a Human Touch
  6. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Models
  7. 2025FMC: Formalization of Natural Language Mathematical Competition Problems
  8. 2025EvolProver: Advancing Automated Theorem Proving by Evolving Formalized Problems via Symmetry and Difficulty