Builds an agent harness that generates and audits Lean 4 proofs, adding axiom audits, fresh review, and independent kernel checking, evaluated on Lean benchmarks.
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.
Problem
Coding agents that write Lean proofs are usually judged by whether the proof compiles. Compilation does not show that the agent kept the intended statement, used only acceptable axioms, avoided reference solutions, or submitted the same artifact that was reviewed.
Approach
FORALL-LEAN-AGENT is a frontend-agnostic harness with adapters for Claude Code, Codex, and OpenCode. Each actor works in an isolated sandbox with Lean MCP tools. A fresh read-only reviewer then recompiles and critiques the candidate. The framework runs statement-integrity and axiom audits (#print axioms), uses an independent comparator/kernel where supported, and binds verifier results and reviewer approval to a single SHA-256 digest of the candidate. Network and filesystem restrictions keep agents away from reference solutions.
Figure 1: The Forall-Lean-Agent workflow. A coding agent develops a candidate in an isolated sandbox using Lean and MCP tools. A fresh reviewer recompiles and assesses the candidate without access to the actor’s transcript. Acceptance binds the verifier result, reviewer approval, and stored artifact to one digest. Axiom auditing checks dependencies, and Lean Eval additionally uses an independent c
Results
On a 100-task VeriSoftBench subset, every Codex and Claude Code configuration reached 100/100 benchmark-rule success; for GPT-5.6 Sol at low effort it rose from 93 to 100 while cost fell from $69 to $62. All 672 PutnamBench problems were accepted at $4.72 average cost. Both Lean Eval software-verification problems were solved and validated by the benchmark.
