Forall-Lean-Agent for Auditable Reasoning in Formal Mathematics and Software Verification

Lean 4 provides a formal language and a trusted kernel for checking mathematical arguments and software properties. General-purpose coding agents can interact with this infrastructure to retrieve declarations, construct proofs, and revise candidates in response to compiler diagnostics. Recent work on general-purpose agents for formal mathematics and minimal theorem-proving agents demonstrates the applicability of this approach without requiring a dedicated prover to be trained for each task.

Successful compilation, however, does not by itself establish that a candidate proves the intended statement under an acceptable axiom policy. A candidate may alter a definition used by the target, inherit an admitted dependency, or differ from the artifact for which verification was recorded. Evaluation therefore requires an explicit protocol connecting proof generation, statement preservation, verification, and acceptance.

We present Forall-Lean-Agent, a frontend-agnostic framework that separates proof construction from framework-controlled verification and fresh review. The framework restricts access to task context, exposes declaration statements through Lean tools, and binds verification evidence and reviewer approval to the same candidate artifact. Adapters support Codex, Claude Code, and OpenCode.

The study makes three contributions. First, it introduces an auditable execution and acceptance protocol. Second, it provides an empirical evaluation that distinguishes benchmark-rule success, strict axiom compliance, and independent-checker coverage. Third, it applies the protocol to competition mathematics, larger formal developments, and repository verification. The evaluations use PutnamBench, the Lean Eval software-verification track, and VeriSoftBench. On PutnamBench, proofs are accepted for all 672 problems in the Lean answer-given configuration. For GPT-5.6 Sol at low effort, integration with the framework increases benchmark-rule success from 93 to 100 on the 100-task VeriSoftBench subset while reducing total cost from $69 to $62.

Agentic proof generation

COPRA uses execution feedback to guide proof generation. Numina-Lean-Agent integrates a general-purpose coding agent with Lean tools for retrieval, compilation, and auxiliary reasoning. Ax-Prover separates orchestration, proving, and verification, while a minimal agent for automated theorem proving examines iterative refinement, library search, and context management. Forall-Lean-Agent builds on these approaches, emphasizing runtime information boundaries and the evidence required to accept a specific candidate.

Evaluation and verification

PutnamBench evaluates formalized competition mathematics. Lean Eval assesses formal developments against trusted challenge statements. Its comparator checks statement agreement and permitted axioms, with support for external kernels such as nanoda. VeriSoftBench preserves repository context and project-specific dependencies in software-verification tasks. The present study applies a common acceptance design across these settings while retaining their distinct task definitions, resource budgets, and verification requirements.

Forall-Lean-Agent coordinates a persistent proof-generating actor, framework-controlled verification, and a fresh reviewer. Figure 1 summarizes the execution protocol. Acceptance is associated with an identified candidate and its verification evidence, rather than with the actor's declaration that a task is complete.

Execution model

Frontend adapters connect the proof-generating model to Lean, while benchmark adapters supply the target statement, build environment, and scoring procedure. This separation permits the same acceptance protocol to operate on Mathlib problems, multi-file developments, and repository theorems. The actor cannot modify framework state or acceptance records.

Workspace isolation

For PutnamBench, the workspace contains the build configuration and compiled Mathlib dependencies without the benchmark checkout containing reference solutions. For repository tasks, the actor receives a sanitized project with proof bodies removed and the target theorem withheld from retrieval. We use runtime blindness to describe these execution-time access restrictions. The term does not imply absence of training-data exposure.

Shell-enabled configurations apply operating-system restrictions across the process tree and use a local proxy that permits outbound traffic only to the model provider. Tool-restricted configurations validate tool names and resolve path arguments before execution. These restrictions prevent access to reference solutions through repository history or previous outputs.

Lean tools and retrieval

Forall-Lean-MCP provides lookup, search, usages, and outline. Responses contain declaration kinds, statements, and source locations without proof bodies. Benchmark-specific tools provide initialization, compilation, and submission. Shell-based adapters can invoke the build and scorer directly while retaining the acceptance protocol.

Statement-only retrieval exposes repository interfaces without revealing completed proofs through that channel. Two exploratory evaluations found that navigation accounted for 51–65% of tool calls and compilation for 10–20%. These observations motivated the interface but do not isolate its effect on proof success.

Candidate review and acceptance

After a verifier pass, a fresh reviewer receives read-only access to the task statement and candidate. It cannot inspect the actor's transcript, previous reviews, or orchestration state. The reviewer recompiles the candidate and checks for statement weakening, declaration shadowing, altered answer values, unsupported assumptions, and vacuous or circular constructions.

Acceptance requires verifier success and reviewer approval for the same candidate, identified by its SHA-256 digest. This prevents verification evidence from being applied to a different version of the proof. Rejected candidates return to the actor with feedback for revision.

Proof generation and revision continue within explicit limits on attempts, time, and cost. A candidate is accepted only after passing both verification and review.

Verification and artifact audit

The verifier screens candidate syntax, preservation of the frozen statement, declaration shadowing, elaboration, and kernel axioms. The syntactic policy rejects admissions, declared axioms, disallowed imports, and mechanisms such as native_decide, @[implemented_by], and @[extern]. Statement comparison disregards whitespace and comments. A separate shadowing guard rejects new bindings that change the interpretation of names used by the target, except declarations already present in the trusted template.

For example, redefining IsGreatest as set membership removes the upper-bound requirement while allowing an apparently unchanged theorem to elaborate. Preservation of the target's surface text is therefore insufficient when its referenced declarations can change.

The axiom audit invokes #print axioms for the target declaration. The strict policy permits only propext, Classical.choice, and Quot.sound. Independent checking additionally compares the candidate with the trusted challenge and checks its exported proof with a separate kernel. The Lean Eval evaluation requires both statement comparison and independent kernel checking.

Accepted proofs are checked again in clean benchmark environments. Proofs, axiom dependencies, and verification evidence are retained for audit. Similarity to reference proofs can guide manual inspection, but does not by itself establish either leakage or independence.

Tasks and coverage

The mathematical evaluation covers 672 problems in the Lean answer-given configuration of PutnamBench. The Lean Eval evaluation covers both strong normalization for the calculus of constructions and quantifier elimination for real closed fields, the two problems in the software-verification track.

The repository evaluation uses the 100-task VeriSoftBench-Aristotle subset drawn from 11 repositories, covering compiler verification, type systems, circuit libraries, probabilistic programs, and separation logic. The full 500-task benchmark was not evaluated.

Configurations and accounting

PutnamBench uses Opus 5 at xhigh effort. Resource statistics cover the 672 accepted proofs. The two Lean Eval developments use GPT-6 Astra.

The target repository protocol is Pass@8 with r = 3, allowing up to eight samples and three local compiler invocations per sample. Reviewer rounds are additional. Within-frontend comparisons fix the model and effort setting, but recorded sampling, compilation, and review budgets differ. The comparisons therefore assess execution protocols without isolating individual component effects or assuming equal budgets.

PutnamBench costs sum the full actor and reviewer expenditure within the 672 retained final task records, including revisions within those runs. Archived or superseded attempts and subsequent toolchain migration work are outside this accounting. Repository-evaluation costs include proof generation, review, and retries.

Outcome measures

Framework acceptance records verifier success and reviewer approval for the same candidate under the configured evaluation protocol. Benchmark-rule success means that the candidate satisfies the benchmark's scoring policy. Strict success additionally requires compliance with the permitted axiom policy. On VeriSoftBench, a candidate can satisfy the benchmark's scoring rule while inheriting sorryAx or native-evaluation dependencies from repository lemmas. It therefore counts as a benchmark-rule success without qualifying as a strict success. Reviewer approval does not remove those inherited dependencies.

Independent-checker acceptance reports accepted candidates over the number judged by that checker. Unchecked candidates count as neither independent passes nor independent failures.

Public benchmark results are available on the PutnamBench leaderboard, the Lean Eval software-verification leaderboard, and the VeriSoftBench model comparison page.

Mathematical verification

PutnamBench

Forall-Lean-Agent achieves 672/672 on PutnamBench using Opus 5 at xhigh effort in the Lean answer-given configuration. Every task has a proof accepted by the verifier and a fresh reviewer. All 672 proofs have been re-verified on Lean 4.33.1.

Of the accepted candidates, 662 receive approval in the first review round and 10 are accepted after one revision. The median number of compiler invocations before acceptance is seven, with a maximum of 56. Mean actor and reviewer costs are $3.52 and $1.20, respectively, giving an average of $4.72 per accepted task and a total of $3,169.41 under the accounting defined above. Figure 2 shows cost against elapsed time and cumulative cost across accepted proofs.

Software verification

Lean Eval

Both Lean Eval software-verification developments pass native compilation, fresh review, comparator validation, and independent-kernel checks under the study's acceptance protocol.

The strong-normalization proof covers all six obligations without a universe bound. Its construction involved human assistance, including strategic guidance, so the result does not establish fully autonomous performance. The real-closed-field implementation has no stated degree or depth restriction.

These results extend the evaluation beyond individual theorem proofs to larger formal developments.

VeriSoftBench

For Codex with GPT-5.6 Sol at low effort, Forall-Lean-Agent increases benchmark-rule success from 93 to 100 and strict success from 82 to 88, while total cost decreases from $69 to $62. Independent checking accepts 63 of the 69 judged candidates in the framework configuration.

Figure 3 presents all 16 reported configurations, including the published Aleph Prover, Aristotle, and Gemini-3-Pro baselines, Numina-Lean-Agent with Claude Code, and runs with Claude Code, Codex, and OpenCode. Benchmark-rule success is shown on a common axis. Model settings, strict success, independent checking, token usage, and recorded cost are available for each configuration where reported.

With Opus 5 at xhigh effort, both configurations attain 100 benchmark-rule successes, but strict success increases from 89 to 96 and cost decreases from $135 to $111. Independent checking accepts all 69 judged candidates in the framework configuration. At the benchmark-rule ceiling, axiom compliance and resource consumption therefore remain informative.

With Fable 5 at low effort, benchmark-rule success increases from 96 to 100, while strict success remains at 89 and cost increases from $157 to $350. These results do not support a uniform cost-reduction claim.

Saturation and coverage

Our results illustrate a limitation of evaluating progress primarily through aggregate solve counts. On the evaluated PutnamBench configuration, proofs are accepted for all 672 tasks. Once a configuration reaches this ceiling, additional improvements in reliability, resource efficiency, or proof quality cannot increase its solve count. Coverage of a fixed task set therefore leaves substantial questions about broader capability unresolved.

The Lean Eval results extend the evaluation to larger formal developments, but two accepted software-verification tasks provide limited evidence about performance across projects. The strong-normalization development also involved human assistance. On the 100-task VeriSoftBench subset, several configurations reach 100 benchmark-rule successes, including Claude Code without Forall-Lean-Agent. This ceiling limits the subset's ability to distinguish those configurations through solve counts alone.

Beyond solve counts

Identical benchmark-rule scores can conceal differences in the guarantees established and the resources consumed. The Opus 5 comparison at xhigh effort in Figure 3 attains the same benchmark-rule score while differing in strict axiom compliance and total cost. Independent checking adds evidence from a separate kernel implementation. Reporting these measures separately preserves information that a single success percentage would obscure.

Task validity and versioning also affect interpretation. Comparisons should identify the exact statements evaluated and retain the corresponding artifacts. Model settings, available context, tool access, sampling budgets, and human assistance also need to be explicit before differences can be attributed to a verification framework.

Evaluation requirements

These observations motivate evaluations that measure reliability under clearly specified resource and verification constraints. Repeated runs with comparable budgets would help distinguish consistent performance from an eventual success obtained through additional attempts. Reporting cost and elapsed time alongside strict verification and independent-checker coverage would preserve meaningful distinctions as solve counts approach their ceiling.

Broader coverage should also test capabilities that this study does not establish, including formulating adequate specifications, maintaining proofs as implementations and dependencies change, and identifying requirements that cannot be satisfied. Lean Eval explicitly distinguishes correctness from readability and reusability, illustrating that passing a verifier need not measure every property required for practical adoption. For critical software, evaluation must connect the validity of the checked statement to the intended requirement, the reliability of proof construction, and the effort required to preserve the guarantee over time.

The evaluation is descriptive. It does not include repeated configurations, confidence intervals, or component ablations, so it does not estimate variability across repeated trials or isolate the contributions of retrieval, review, and continuation.

The reviewer shares the actor's model family. Separate contexts therefore do not establish statistically independent errors. Reviewer approval supplements formal verification evidence. Formal correctness remains conditional on the verifier, its trusted environment, and the adequacy of the specification. Acceptance does not certify that a proof is minimal, idiomatic, or reusable.

Runtime information restrictions cannot rule out training-data exposure. Temporal holdouts and withheld solutions would strengthen contamination studies. Limited disclosure by closed-source baselines restricts comparisons of capability and efficiency, while the unreleased framework limits external reproduction.

Broader impacts

Automated Lean proving may reduce the effort required for formal verification. Proofs of inadequate specifications can nevertheless create unwarranted confidence in unsafe systems. Statement comparison, axiom audits, and human specification review address distinct parts of this risk. The present results support evaluation of auditable proof artifacts. They do not establish safety properties beyond the formal statements checked.

Forall-Lean-Agent links persistent proof generation and fresh review to verified artifacts through a frontend-agnostic execution and acceptance protocol. Isolated workspaces, statement-aware verification, axiom audits, and candidate digests make the evidence underlying acceptance traceable.

The evaluation accepts proofs for all 672 PutnamBench tasks, supports both independently checked Lean Eval software-verification developments, and demonstrates strong performance on the 100-task VeriSoftBench subset. Improvements in correctness and efficiency depend on the configuration. These findings support reporting accepted artifacts alongside verification policies, information boundaries, and resource budgets, rather than relying on aggregate solve counts alone.

This project was led by Naing Oo Lwin. We thank Hung Pham, Todd Schmid, Jules Jacobs, and Wojciech Różowski for their advice and guidance. We also thank George Tsoukalas and Jocelyn Qiaochu Chen for supporting our submissions to PutnamBench and VeriSoftBench, respectively, and for helping verify and review the results. We are grateful to the anonymous reviewers at NeurIPS VeriCodeGen for their thoughtful feedback.