Framework improves checking and trust in automated Lean proofs
FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification
Software EngineeringArtificial IntelligenceLogic in Computer Science
Summary
Automated computer programs can help write complicated math and software proofs using a system called Lean, but just finishing a proof doesn't guarantee it's actually correct. The authors created a new system called FORALL-LEAN-AGENT that helps check these proofs more carefully and makes it easy to audit the reasoning behind them. Their system uses separate work areas, special tools, and independent checks to make sure proofs follow the rules and assumptions properly. They tested it on several challenging sets of problems and found that it improved success rates and lowered costs when using AI agents to generate the proofs.
What this means in practice
- •For software verification engineers: Use the system to validate and audit automatically generated proofs ensuring software correctness properties hold under accepted assumptions.
- •For formal methods practitioners: Integrate the framework to improve reliability and traceability of formal proofs produced by AI agents in mathematical theorem proving workflows.
Authors
Naing Oo Lwin
Abstract
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.