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.
Keywords
Subject
Publication details
- Journal
- Not available
- Open access
- Green open access
Cite this article
APA 7
Lwin, N. O. (2026). FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification. https://omanscience.com/en/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification
MLA 9
Lwin, Naing Oo. "FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification." https://omanscience.com/en/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification.
Chicago (author–date)
Lwin, Naing Oo. 2026. "FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification." https://omanscience.com/en/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification.
Harvard
Lwin, N. O. (2026) 'FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification', Available at: https://omanscience.com/en/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification.
Vancouver
Lwin NO. FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification. https://omanscience.com/en/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification
IEEE
N. O. Lwin, "FORALL-LEAN-AGENT for Auditable Reasoning in Formal Mathematics and Software Verification," https://omanscience.com/en/articles/forall-lean-agent-for-auditable-reasoning-in-formal-mathematics-and-software-verification.