mlsanityData to 7 Oct 2026

Learning to Prove Theorems via Interacting with Proof Assistants

arXiv 1905.09381 ↗First posted 21 May 2019cs.LO cs.AI cs.LGcited by 107

Not on the map. Why?

Abstract (arXiv)

Humans prove theorems by relying on substantial high-level reasoning and problem-specific insights. Proof assistants offer a formalism that resembles human mathematical reasoning, representing theorems in higher-order logic and proofs as high-level tactics. However, human experts have to construct proofs manually by entering tactics into the proof assistant. In this paper, we study the problem of using machine learning to automate the interaction with proof assistants. We construct CoqGym, a large-scale dataset and learning environment containing 71K human-written proofs from 123 projects developed with the Coq proof assistant. We develop ASTactic, a deep learning-based model that generates tactics as programs in the form of abstract syntax trees (ASTs). Experiments show that ASTactic trained on CoqGym can generate effective tactics and can be used to prove new theorems not previously provable by automated methods. Code is available at https://github.com/princeton-vl/CoqGym.

Key facts. Cited by 107 papers in the map (data through 7 Oct 2026). First posted on arXiv 21 May 2019.

Builds on

No reference list yet.

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2021: 11; 2022: 7; 2023: 15; 2024: 36; 2025: 20; 2026: 18.

107 papers.

Sort:

By area:

  1. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
  2. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  3. 2024Large Language Models for Mathematical Reasoning: Progresses and Challengescited by 283
  4. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  5. 2023ProofNet: Autoformalizing and Formally Proving Undergraduate-Level Mathematicscited by 180
  6. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  7. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  8. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  9. 2022A Survey of Deep Learning for Mathematical Reasoningcited by 124
  10. 2023Baldur: Whole-Proof Generation and Repair with Large Language Modelscited by 118
  11. 2024Lean Workbook: A large-scale Lean problem set formalized from natural language math problemscited by 115
  12. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
38 more
  1. 2021NaturalProofs: Mathematical Theorem Proving in Natural Languagecited by 80
  2. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  3. 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
  4. 2024TheoremLlama: Transforming General-Purpose LLMs into Lean4 Expertscited by 58
  5. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  6. 2024DafnyBench: A Benchmark for Formal Software Verificationcited by 54
  7. 2022Generating Natural Language Proofs with Verifier-Guided Searchcited by 52
  8. 2024Lean Copilot: Large Language Models as Copilots for Theorem Proving in Leancited by 52
  9. 2023Magnushammer: A Transformer-Based Approach to Premise Selectioncited by 50
  10. 2021LIME: Learning Inductive Bias for Primitives of Mathematical Reasoningcited by 46
  11. 2024AutoVerus: Automated Proof Generation for Rust Codecited by 46
  12. 2024Process-Driven Autoformalization in Lean 4cited by 45
  13. 2021TacticZero: Learning to Prove Theorems from Scratch with Deep Reinforcement Learningcited by 37
  14. 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
  15. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  16. 2025RealMath: A Continuous Benchmark for Evaluating Language Models on Research-Level Mathematicscited by 30
  17. 2024Autoformalizing Euclidean Geometrycited by 27
  18. 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
  19. 2024LEAN-GitHub: Compiling GitHub LEAN repositories for a versatile LEAN provercited by 25
  20. 2024Rango: Adaptive Retrieval-Augmented Proving for Automated Software Verificationcited by 25
  21. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24
  22. 2023TRIGO: Benchmarking Formal Mathematical Proof Reduction for Generative Language Modelscited by 24
  23. 2023Mathematical Language Models: A Surveycited by 24
  24. 2025Solving Inequality Proofs with Large Language Modelscited by 21
  25. 2024Proving Olympiad Algebraic Inequalities without Human Demonstrationscited by 20
  26. 2024Proof Automation with Large Language Modelscited by 20
  27. 2024Towards Neural Synthesis for SMT-Assisted Proof-Oriented Programmingcited by 19
  28. 2024miniCodeProps: a Minimal Benchmark for Proving Code Propertiescited by 18
  29. 2025Proving the Coding Interview: A Benchmark for Formally Verified Code Generationcited by 18
  30. 2021Contrastive Reinforcement Learning of Symbolic Reasoning Domainscited by 17
  31. 2023Can Transformers Learn to Solve Problems Recursively?cited by 17
  32. 2025From Informal to Formal -- Incorporating and Evaluating LLMs on Natural Language Requirements to Verifiable Formal Proofscited by 17
  33. 2024Graph2Tac: Online Representation Learning of Formal Math Conceptscited by 15
  34. 2024Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4cited by 15
  35. 2024Transformer-Based Models Are Not Yet Perfect At Learning to Emulate Structural Recursioncited by 14
  36. 2025miniF2F-Lean Revisited: Reviewing Limitations and Charting a Path Forwardcited by 13
  37. 2025A Survey on Mathematical Reasoning and Optimization with Large Language Modelscited by 12
  38. 2023Leveraging Large Language Models for Automated Proof Synthesis in Rustcited by 11

50 most cited of 107 All 107 (JSON)