FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
On the map: LLM agents and tool use → Software engineering coding agents
Abstract (arXiv)
Coding agents increasingly automate Lean proof development, but successful compilation alone does not establish that a candidate proves the intended statement under acceptable assumptions. We present FORALL-LEAN-AGENT, a frontend-agnostic framework for auditable reasoning in formal mathematics and software verification. The framework combines isolated workspaces, Lean tools, and fresh review with statement comparison, axiom audits, and independent proof checking where supported. Verification evidence and reviewer decisions are bound to the same candidate artifact, making acceptance traceable. We evaluate the framework on VeriSoftBench, PutnamBench, and both problems in the Lean Eval softwareverification track. On the 100-task VeriSoftBench subset, integration with FORALLLEAN-AGENT raises benchmark-rule success from 93 to 100 for GPT-5.6 Sol at low effort while reducing cost from 69 to 62. The PutnamBench evaluation accepts all 672 problems at an average of 4.72 each. These results show that agent harness design can improve correctness and efficiency while providing evidence beyond aggregate solve counts.
Key facts. No citing papers in the map yet (data through 7 Oct 2026). Placed in Software engineering coding agents, one of 16 directions in LLM agents and tool use. Builds on 18 of its 27 references that are in the map. First posted on arXiv 1 Oct 2026.
Builds on
18 of 27 references.
References · 18
- 2023LeanDojo: Theorem Proving with Retrieval-Augmented Language Modelscited by 414
- 2024PutnamBench: Evaluating Neural Theorem-Provers on the Putnam Mathematical Competitioncited by 153
- 2025Goedel-Prover-V2: Scaling Formal Theorem Proving with Scaffolded Data Synthesis and Self-Correctioncited by 140
- 2023An In-Context Learning Agent for Formal Theorem-Provingcited by 78
- 2025Hilbert: Recursively Building Formal Proofs with Informal Reasoningcited by 55
- 2025Aristotle: IMO-level Automated Theorem Provingcited by 47
- 2026Numina-Lean-Agent: An Open and General Agentic Reasoning System for Formal Mathematicscited by 43
- 2025Seed-Prover 1.5: Mastering Undergraduate-Level Theorem Proving via Learning from Experiencecited by 36
- 2024miniCTX: Neural Theorem Proving with (Long-)Contextscited by 35
- 2025Ax-Prover: A Deep Reasoning Agentic Framework for Theorem Proving in Mathematics and Quantum Physicscited by 27
- 2025A benchmark for vericoding: formally verified program synthesiscited by 16
- 2024Pantograph: A Machine-to-Machine Interaction Interface for Advanced Theorem Proving, High Level Reasoning, and Data Extraction in Lean 4cited by 15
6 more
- 2026A Minimal Agent for Automated Theorem Provingcited by 13
- 2026Goedel-Code-Prover: Hierarchical Proof Search for Open State-of-the-Art Code Verificationcited by 10
- 2026Goedel-Architect: Streamlining Formal Theorem Proving with Blueprint Generation and Refinementcited by 7
- 2026VeriSoftBench: Repository-Scale Formal Verification Benchmarks for Leancited by 6
- 2026Agentic Proving for Program Verificationcited by 3
- 2026Harnessing Code Agents for Automatic Software Verificationcited by 1
Built on by
Not cited yet.
Similar, not cited
Close in wording, no citation either way
- 2026Self-Modifying Lean Proof Agents with Verifier-Grounded Benchmark Coevolution
- 2026SorryDB: Can AI Provers Complete Real-World Lean Theorems?
- 2026OProver: A Unified Framework for Agentic Formal Theorem Proving
- 2026Optimizing the Cost-Quality Tradeoff of Agentic Theorem Provers in Lean
- 2026Automating Formal Verification with Agent-Guided Tree Search
- 2026LEAP: Supercharging LLMs for Formal Mathematics with Agentic Frameworks
- 2026Beyond the Library: An Agentic Framework for Autoformalizing Research Mathematics
- 2025APOLLO: Automated LLM and Lean Collaboration for Advanced Formal Reasoning