mlsanityData to 7 Oct 2026

A Survey on Deep Learning for Theorem Proving

arXiv 2404.09939 ↗First posted 15 Apr 2024cs.AIcited by 55

Not on the map. Why?

Abstract (arXiv)

Theorem proving is a fundamental aspect of mathematics, spanning from informal reasoning in natural language to rigorous derivations in formal systems. In recent years, the advancement of deep learning, especially the emergence of large language models, has sparked a notable surge of research exploring these techniques to enhance the process of theorem proving. This paper presents a comprehensive survey of deep learning for theorem proving by offering (i) a thorough review of existing approaches across various tasks such as autoformalization, premise selection, proofstep generation, and proof search; (ii) an extensive summary of curated datasets and strategies for synthetic data generation; (iii) a detailed analysis of evaluation metrics and the performance of state-of-the-art methods; and (iv) a critical discussion on the persistent challenges and the promising avenues for future exploration. Our survey aims to serve as a foundational reference for deep learning approaches in theorem proving, inspiring and catalyzing further research endeavors in this rapidly growing field. A curated list of papers is available at https://github.com/zhaoyu-li/DL4TP.

Key facts. Cited by 55 papers in the map (data through 7 Oct 2026). Builds on 149 of its 259 references that are in the map. First posted on arXiv 15 Apr 2024.

Builds on

149 of 259 references.

References · 149

  1. 2017Attention Is All You Needcited by 59,932
  2. 2018BERT: Pre-training of Deep Bidirectional Transformers for Language Understandingcited by 40,204
  3. 2020Language Models are Few-Shot Learnerscited by 32,199
  4. 2023GPT-4 Technical Reportcited by 18,132
  5. 2019RoBERTa: A Robustly Optimized BERT Pretraining Approachcited by 13,266
  6. 2020A Simple Framework for Contrastive Learning of Visual Representationscited by 11,979
  7. 2017Graph Attention Networkscited by 8,854
  8. 2024DeepSeekMath: Pushing the Limits of Mathematical Reasoning in Open Language Modelscited by 8,851
  9. 2021Evaluating Large Language Models Trained on Codecited by 8,053
  10. 2018Representation Learning with Contrastive Predictive Codingcited by 7,662
  11. 2022PaLM: Scaling Language Modeling with Pathwayscited by 5,304
  12. 2018How Powerful are Graph Neural Networks?cited by 4,355
38 more
  1. 2014Learning Phrase Representations using RNN Encoder-Decoder for Statistical Machine Translationcited by 4,016
  2. 2020Dense Passage Retrieval for Open-Domain Question Answeringcited by 3,779
  3. 2013Playing Atari with Deep Reinforcement Learningcited by 3,211
  4. 2014Sequence to Sequence Learning with Neural Networkscited by 2,974
  5. 2016WaveNet: A Generative Model for Raw Audiocited by 1,710
  6. 2022Solving Quantitative Reasoning Problems with Language Modelscited by 1,359
  7. 2017Hindsight Experience Replaycited by 1,096
  8. 2019Cross-lingual Language Model Pretrainingcited by 1,088
  9. 2020MPNet: Masked and Permuted Pre-training for Language Understandingcited by 973
  10. 2015Convolutional Networks on Graphs for Learning Molecular Fingerprintscited by 751
  11. 2021ByT5: Towards a token-free future with pre-trained byte-to-byte modelscited by 504
  12. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  13. 2023Llemma: An Open Language Model For Mathematicscited by 385
  14. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  15. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  16. 2023Logic-LM: Empowering Large Language Models with Symbolic Solvers for Faithful Logical Reasoningcited by 379
  17. 2022Language Models Are Greedy Reasoners: A Systematic Formal Analysis of Chain-of-Thoughtcited by 334
  18. 2020ProofWriter: Generating Implications, Proofs, and Abductive Statements over Natural Languagecited by 309
  19. 2015Improved Semantic Representations From Tree-Structured Long Short-Term Memory Networkscited by 305
  20. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  21. 2020Transformers as Soft Reasoners over Languagecited by 265
  22. 2023Mathematical Capabilities of ChatGPTcited by 263
  23. 2022Autoformalization with Large Language Modelscited by 252
  24. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  25. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  26. 2023LINC: A Neurosymbolic Approach for Logical Reasoning by Combining Language Models with First-Order Logic Proverscited by 161
  27. 2023OpenWebMath: An Open Dataset of High-Quality Mathematical Web Textcited by 151
  28. 2021Explaining Answers with Entailment Treescited by 148
  29. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  30. 2018Phrase-Based & Neural Unsupervised Machine Translationcited by 138
  31. 2022UniGeo: Unifying Geometry Logical Reasoning via Reformulating Mathematical Expressioncited by 137
  32. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  33. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  34. 2024InternLM-Math: Open Math Large Language Models Toward Verifiable Reasoningcited by 117
  35. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  36. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  37. 2023GeomVerse: A Systematic Evaluation of Large Models for Geometric Reasoningcited by 107
  38. 2023SatLM: Satisfiability-Aided Language Models Using Declarative Promptingcited by 100

50 most cited of 149 All 149 (JSON)

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2024: 13; 2025: 27; 2026: 15.

55 papers.

Sort:

By area:

  1. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  2. 2024A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challengescited by 55
  3. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  4. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  5. 2024AlphaVerus: Bootstrapping Formally Verified Code Generation through Self-Improving Translation and Treefinementcited by 33
  6. 2024Autoformalizing Euclidean Geometrycited by 27
  7. 2025PDE-Controller: LLMs for Autoformalization and Reasoning of PDEscited by 23
  8. 2024FVEL: Interactive Formal Verification Environment with Large Language Models via Theorem Provingcited by 22
  9. 2026Large Language Model Reasoning Failurescited by 20
  10. 2024FormalAlign: Automated Alignment Evaluation for Autoformalizationcited by 19
  11. 2025Autoformalization in the Era of Large Language Models: A Surveycited by 19
  12. 2025ReForm: Reflective Autoformalization with Prospective Bounded Sequence Optimizationcited by 18
38 more
  1. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 17
  2. 2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
  3. 2025Reviving DSP for Advanced Theorem Proving in the Era of Reasoning Modelscited by 17
  4. 2025StepFun-Formalizer: Unlocking the Autoformalization Potential of LLMs through Knowledge-Reasoning Fusioncited by 15
  5. 2025VeruSAGE: A Study of Agent-Based Verification for Rust Systemscited by 11
  6. 2024Laurel: Unblocking Automated Verification with Large Language Modelscited by 10
  7. 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 10
  8. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 8
  9. 2025From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systemscited by 8
  10. 2025Faithful and Robust LLM-Driven Theorem Proving for NLI Explanationscited by 8
  11. 2025Autoformalizer with Tool Feedbackcited by 7
  12. 2025Knowledge Augmented Complex Problem Solving with Large Language Models: A Surveycited by 6
  13. 2025StepProof: Step-by-step verification of natural language mathematical proofscited by 6
  14. 2025FormalML: A Benchmark for Evaluating Formal Subgoal Completion in Machine Learning Theorycited by 5
  15. 2025Agentic Verification of Software Systemscited by 5
  16. 2025Scalable Oversight for Superhuman AI via Recursive Self-Critiquingcited by 4
  17. 2025A Survey of Deep Learning for Geometry Problem Solvingcited by 4
  18. 2025Towards Repository-Level Program Verification with Large Language Modelscited by 4
  19. 2026Learning to Disprove: Formal Counterexample Generation with Large Language Modelscited by 4
  20. 2026DreamProver: Evolving Transferable Lemma Libraries via a Wake-Sleep Theorem-Proving Agentcited by 4
  21. 2024Alchemy: Amplifying Theorem-Proving Capability through Symbolic Mutationcited by 3
  22. 2024Library Learning Doesn't: The Curious Case of the Single-Use "Library"cited by 3
  23. 2025RAG-Verus: Repository-Level Program Verification with LLMs using Retrieval Augmented Generationcited by 3
  24. 2025LeanTutor: Towards a Verified AI Mathematical Proof Tutorcited by 3
  25. 2025Translating Informal Proofs into Formal Proofs Using a Chain of Statescited by 3
  26. 2026Theory-Scale Auto-Formalization of Logics for Computer Sciencecited by 3
  27. 2024RoMath: A Mathematical Reasoning Benchmark in Romaniancited by 2
  28. 2025Beyond Theorem Proving: Formulation, Framework and Benchmark for Formal Problem-Solvingcited by 2
  29. 2025Improving Autoformalization Using Direct Dependency Retrievalcited by 2
  30. 2025MSC-180: A Benchmark for Automated Formal Theorem Proving from Mathematical Subject Classificationcited by 2
  31. 2026CDRL: Certification-Driven Reinforcement Learning for Neutrino Flavor Model Discoverycited by 2
  32. 2025G"odel's Poetrycited by 1
  33. 2026Neuro-Symbolic Proof Generation for Scaling Systems Software Verificationcited by 1
  34. 2026Hilbert-Geo: Solving Solid Geometric Problems by Neural-Symbolic Reasoningcited by 1
  35. 2026LAMP: Lean-based Agentic framework with MCP and Proof Repaircited by 1
  36. 2026From Solvers to Research: Large Language Model-Driven Formal Mathematics at the Research Frontiercited by 1
  37. 2026Does the Proof Prove It That Way? Faithful Formalization of Elements Proofscited by 1
  38. 2025An Ontology-Based Approach to Optimizing Geometry Problem Sets for Skill Developmentcited by 0

50 most cited of 55 All 55 (JSON)