mlsanityData to 7 Oct 2026

An In-Context Learning Agent for Formal Theorem-Proving

arXiv 2310.04353 ↗First posted 6 Oct 2023cs.LG cs.AI cs.LOcited by 78

On the map: LLM agents and tool use → Educational agents and math problem solving

Abstract (arXiv)

We present an in-context learning agent for formal theorem-proving in environments like Lean and Coq. Current state-of-the-art models for the problem are finetuned on environment-specific proof data. By contrast, our approach, called COPRA, repeatedly asks a high-capacity, general-purpose large language model (GPT-4) to propose tactic applications from within a stateful backtracking search. Proposed tactics are executed in the underlying proof environment. Feedback from the execution is used to build the prompt for the next model query, along with selected information from the search history and lemmas retrieved from an external database. We evaluate our implementation of COPRA on the miniF2F benchmark for Lean and a set of Coq tasks from the CompCert project. On these benchmarks, COPRA significantly outperforms few-shot invocations of GPT-4. It also compares favorably against finetuning-based approaches, outperforming ReProver, a state-of-the-art finetuned approach for Lean, in terms of the pass@1 metric. Our code and data are available at https://github.com/trishullab/copra.

Key facts. Cited by 78 papers in the map (data through 7 Oct 2026). Placed in Educational agents and math problem solving, one of 16 directions in LLM agents and tool use. Builds on 26 of its 38 references that are in the map. First posted on arXiv 6 Oct 2023.

Builds on

26 of 38 references.

References · 26

  1. 2020Language Models are Few-Shot Learnerscited by 32,199
  2. 2023LLaMA: Open and Efficient Foundation Language Modelscited by 13,958
  3. 2022Chain-of-Thought Prompting Elicits Reasoning in Large Language Modelscited by 12,302
  4. 2022ReAct: Synergizing Reasoning and Acting in Language Modelscited by 8,355
  5. 2021Measuring Mathematical Problem Solving With the MATH Datasetcited by 5,203
  6. 2021Zero-Shot Text-to-Image Generationcited by 4,276
  7. 2023Toolformer: Language Models Can Teach Themselves to Use Toolscited by 4,072
  8. 2023Reflexion: Language Agents with Verbal Reinforcement Learningcited by 4,064
  9. 2023Tree of Thoughts: Deliberate Problem Solving with Large Language Modelscited by 3,155
  10. 2023Code Llama: Open Foundation Models for Codecited by 2,105
  11. 2023Voyager: An Open-Ended Embodied Agent with Large Language Modelscited by 2,081
  12. 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
14 more
  1. 2021MiniF2F: a cross-system benchmark for formal Olympiad-level mathematicscited by 380
  2. 2020Generative Language Modeling for Automated Theorem Provingcited by 379
  3. 2022Draft, Sketch, and Prove: Guiding Formal Theorem Provers with Informal Proofscited by 278
  4. 2022HyperTree Proof Search for Neural Theorem Provingcited by 192
  5. 2022Formal Mathematics Statement Curriculum Learningcited by 141
  6. 2021Proof Artifact Co-training for Theorem Proving with Language Modelscited by 130
  7. 2019The Lean mathematical librarycited by 127
  8. 2023LEGO-Prover: Neural Theorem Proving with Growing Librariescited by 108
  9. 2019Learning to Prove Theorems via Interacting with Proof Assistantscited by 107
  10. 2022Thor: Wielding Hammers to Integrate Language Models and Automated Theorem Proverscited by 97
  11. 2018GamePad: A Learning Environment for Theorem Provingcited by 48
  12. 2023Decomposing the Enigma: Subgoal-based Demonstration Learning for Formal Theorem Provingcited by 37
  13. 2019Generating Correctness Proofs with Neural Networkscited by 36
  14. 2023Lyra: Orchestrating Dual Correction in Automated Theorem Provingcited by 24

Built on by

Cited by year (2026 to 7 Oct)

Citing papers per year: 2023: 1; 2024: 15; 2025: 26; 2026: 36.

78 papers.

Sort:

By area:

  1. 2025AlphaEvolve: A coding agent for scientific and algorithmic discoverycited by 763
  2. 2024RepairAgent: An Autonomous, LLM-Based Agent for Program Repaircited by 225
  3. 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
  4. 2024Formal Mathematical Reasoning: A New Frontier in AIcited by 80
  5. 2024Lean-STaR: Learning to Interleave Thinking and Provingcited by 64
  6. 2024A Survey on Deep Learning for Theorem Provingcited by 55
  7. 2024A Survey of Mathematical Reasoning in the Era of Multimodal Large Language Model: Benchmark, Method & Challengescited by 55
  8. 2024The Limits of Inference Scaling Through Resamplingcited by 51
  9. 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
  10. 2024You Name It, I Run It: An LLM Agent to Execute Tests of Arbitrary Projectscited by 45
  11. 2025Solving Formal Math Problems by Decomposition and Iterative Reflectioncited by 35
  12. 2024LeanAgent: Lifelong Learning for Formal Theorem Provingcited by 34
38 more
  1. 2023LLMSTEP: LLM proofstep suggestions in Leancited by 32
  2. 2025VERINA: Benchmarking Verifiable Code Generationcited by 30
  3. 2025Prover Agent: An Agent-Based Framework for Formal Mathematical Proofscited by 28
  4. 2025CLEVER: A Curated Benchmark for Formally Verified Code Generationcited by 27
  5. 2024Proving Theorems Recursivelycited by 25
  6. 2026Large Language Model Reasoning Failurescited by 20
  7. 2025Aria: An Agent For Retrieval and Iterative Auto-Formalization via Dependency Graphcited by 18
  8. 2025Proving Olympiad Inequalities by Synergizing LLMs and Symbolic Reasoningcited by 17
  9. 2025ProofBridge: Auto-Formalization of Natural Language Proofs in Lean via Joint Embeddingscited by 16
  10. 2024Hierarchical Context Pruning: Optimizing Real-World Code Completion with Repository-Level Pretrained Code LLMscited by 13
  11. 2025MATP-BENCH: Can MLLM Be a Good Automated Theorem Prover for Multimodal Problems?cited by 13
  12. 2026A Minimal Agent for Automated Theorem Provingcited by 13
  13. 2026AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithmscited by 11
  14. 2025ProofAug: Efficient Neural Theorem Proving via Fine-grained Proof Structure Analysiscited by 10
  15. 2025LeanProgress: Guiding Search for Neural Theorem Proving via Proof Progress Predictioncited by 9
  16. 2025Grammars of Formal Uncertainty: When to Trust LLMs in Automated Reasoning Taskscited by 9
  17. 2024Cobblestone: A Divide-and-Conquer Approach for Automating Formal Verificationcited by 8
  18. 2025From Hypothesis to Publication: A Comprehensive Survey of AI-Driven Research Support Systemscited by 8
  19. 2025Faithful and Robust LLM-Driven Theorem Proving for NLI Explanationscited by 8
  20. 2025DRIFT: Decompose, Retrieve, Illustrate, then Formalize Theoremscited by 8
  21. 20243D-Prover: Diversity Driven Theorem Proving With Determinantal Point Processescited by 6
  22. 2025GenoMAS: A Multi-Agent Framework for Scientific Discovery via Code-Driven Gene Expression Analysiscited by 6
  23. 2026VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Leancited by 6
  24. 2026RMA: an Agentic System for Research-Level Mathematical Problemscited by 6
  25. 2025MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Studycited by 5
  26. 2025Agentic Verification of Software Systemscited by 5
  27. 2026AXLE: A Cloud Infrastructure for Lean 4 Theorem Proving Utilitiescited by 4
  28. 2024QEDCartographer: Automating Formal Verification Using Reward-Free Reinforcement Learningcited by 3
  29. 2025A Llama walks into the 'Bar': Efficient Supervised Fine-Tuning for Legal Reasoning in the Multi-state Bar Examcited by 3
  30. 2025LeanTutor: Towards a Verified AI Mathematical Proof Tutorcited by 3
  31. 2025ProofCompass: Enhancing Specialized Provers with LLM Guidancecited by 3
  32. 2026Inductive Deductive Synthesis: Enabling AI to Generate Formally Verified Systemscited by 3
  33. 2026Agentic Proving for Program Verificationcited by 3
  34. 2026Theory-Scale Auto-Formalization of Logics for Computer Sciencecited by 3
  35. 2025Discovering New Theorems via LLMs with In-Context Proof Learning in Leancited by 2
  36. 2025Learning Interestingness in Automated Mathematical Theory Formationcited by 2
  37. 2025MINIF2F-DAFNY: LLM-Guided Mathematical Theorem Proving via Auto-Active Verificationcited by 2
  38. 2026Automated Lemma Discovery in Agentic Program Verificationcited by 2

50 most cited of 78 All 78 (JSON)

Similar, not cited

Close in wording, no citation either way

  1. 2026OProver: A Unified Framework for Agentic Formal Theorem Proving
  2. 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoning
  3. 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
  4. 2026Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation
  5. 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experience
  6. 2026Magenta: Closing the Loop Between Mathematical Reasoning and Lean Verification
  7. 2024ImProver: Agent-Based Automated Proof Optimization
  8. 2026Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean