Scaling Lean Theorem Proving for Real-World Code Verification

AI summary

Overview

Research area: Automated theorem proving and formal verification — specifically LLM-driven proof search in Lean 4 applied to both competition mathematics and real program correctness.

Technical level: Advanced. The paper assumes familiarity with proof assistants, LLM agents, and program-verification concepts, though the high-level argument is accessible.

Scope: The paper introduces EasyProver, an agentic Lean proving harness built around an off-the-shelf frontier model, and Aegis, a pipeline that converts competitive programming problems into hard, kernel-checked Lean verification tasks.

What This Paper Is About

Existing formal-reasoning benchmarks for LLMs are running out of headroom — several are near saturation — while the verified-programming benchmarks that remain are small and expensive to author by hand. The authors build a proving system that nearly exhausts the established benchmarks without any model training, then build a generator that manufactures much harder verification tasks from translated real implementations, so progress can still be measured.

Key Contributions

1. EasyProver, a Lean proving runtime combining recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and InfiniLean, a stateless, elastically scaled Lean elaboration service. It uses an off-the-shelf frontier model with no fine-tuning and no separately trained policy or value network.
2. Near-saturation results on established benchmarks: 669/672 PutnamBench (99.6%), all six IMO 2026 formalizations, 597/600 NTP4VC verification conditions (99.5%), and all 189 VERINA tasks, resolved by kernel-checked proof or refutation.
3. Aegis, an automatic pipeline that writes safe Rust solutions to LeetCode problems, translates them to Lean via Charon and Aeneas, generates candidate specifications, and labels each frozen statement with a kernel-checked proof or refutation.
4. A dataset far from saturation: 2,045 differentially validated Rust–Lean program pairs and 11,533 candidate specifications, on which the same prover resolves only 52.7% of a 2,000-statement sample.

Main Findings

• PutnamBench: EasyProver solves 669 of 672 problems (99.6%), which the authors report as 72 more than the strongest configuration in Chung et al. (597/672).
• Competition mathematics: All six IMO 2026 formalizations and all twelve Putnam 2025 problems are solved in a single run. The paper explicitly notes it did not evaluate EasyProver on IMO 2025 or USAMO 2026; those columns show other systems' published results.
• miniF2F: Reported at 99.6 in Table 1 for EasyProver's single run.
• Code verification: All 189 VERINA tasks and all 77 AlgoVeri tasks are resolved; NTP4VC reaches 597/600 (99.5%), comprising 588 proofs and 9 refutations; CLEVER reaches 113 of the 143 tasks that translate to the Lean 4.32 toolchain (79.0%).
• Aegis scale and difficulty: Of 2,356 problems attempted, 2,045 (86.8%) passed every stage — Rust testing, extraction, translation, Lean elaboration, and differential evaluation — yielding 11,533 candidate specifications over 1,257 translated programs in the sample.
• Aegis proof rate: On 1,997 attempted statements from the 2,000-statement stratified sample, EasyProver proved 1,054 (52.7%) within a 30-minute budget per statement and left 943 unresolved.
• Difficulty stratification: Proof rates range from 84.1% for edge-case specifications down to 31.0% for explicit contracts, and from 66.7% on Easy LeetCode problems to 37.6% on Hard ones.
• Proof search scale: The hardest proofs used more than 300 sub-agents in a single run. Per-process semaphores cap active sub-agents at 64 and concurrent expensive Lean queries at 16.
• Elaboration latency: With InfiniLean, imports take tens of seconds while elaboration on a warm worker takes about 0.2 s.
• Proof artifact size: The 1,054 accepted proofs occupy 145,646 physical lines, with a median of 104 lines and a largest artifact of 1,167 lines.
• Anti-reward-hacking guarantees: The statement prefix is frozen, final acceptance requires compiling without sorry and using only allowlisted axioms (checked by Lean Comparator via lake env lean and #print axioms), and in Aegis a separate specification agent writes each statement before the prover sees it.
• Explicit caveat: The model's training cutoff is not public, so contamination of competition-problem solutions cannot be ruled out; the Aegis statements, by contrast, did not exist before this work.
• No ablation: The authors state they do not ablate harness components, and do not compare against the same model using Lean as a tool without the harness.

Methodology in Plain English

EasyProver wraps a general-purpose frontier model in a runtime that behaves like a small research team. A parent agent reads the current proof state and its children's returned results, then decides which branches to continue, revise, or expand — a language-model-driven analogue of tree search, but reading actual returned proofs and counterexamples rather than averaged value estimates.

Each child gets a fresh context and a private copy of the project, so a helper lemma can come back to the parent without dragging along the failed attempts and diagnostics behind it. Finished results arrive at the parent's next turn without waiting for unfinished siblings. Within a single attempt, a tactic prober fires several candidate tactics and automation tools concurrently at the current goal and returns only the winner, so a 30-token tactic need not cost 30,000 tokens of probe traces in context.

Because recursive delegation can swamp a single Lean server, elaboration is moved to InfiniLean: a stateless service that accepts Lean source over JSON-RPC across a load-balanced Kubernetes pool of replicas with Mathlib preloaded, so any replica can serve any request. Final acceptance is deliberately separate from search — candidate proofs are promoted under a lock and independently recompiled by Lean Comparator.

For Aegis, the pipeline has distinct agents with distinct jobs. A coding agent writes safe Rust for LeetCode problems restricted to single pure functions over first-order data; each program is differentially validated by running cargo test, extracting with Charon, translating with Aeneas, and confirming that Lean evaluation matches the Rust outputs on the same inputs. A specification agent then sees the problem, the extracted Lean program, its signature, and validated examples, and writes an elaborating theorem statement with a sorry body, some requested to hold and some requested to fail. An optional Plausible screen tries to find counterexamples before proof search. The statement is frozen, and the prover must establish either it or its negation, which simultaneously grades the specification's requested polarity.

Why This Matters

Research impact: The paper separates two things the field often conflates — the proving harness and the benchmark — and shows that one can be near-saturated while the other is barely half-solved. Because Aegis labels are kernel-checked and the pipeline needs no expert annotation, tasks can be regenerated with more compute, which is a structural answer to contamination rather than a detection heuristic.

Real-world applications:

• Verifying systems code: The obligation types Aegis induces — fixed-width overflow, bounds checks, explicit failure, generated loops, casts, and functionalized mutation — are exactly the ones that show up when verifying real Rust.
• RLVR reward generation: Kernel-checked proofs and refutations provide cheap, recheckable positive and negative labels, unlike tests, which give only finite evidence and can be gamed.
• Benchmarking other provers: The frozen statements and declared trust policies let anyone recheck a label and compare systems on a non-saturated task set.
• Mutation testing: Small edits to a validated program produce plausible but incorrect variants whose specifications yield further negative labels (generated but not evaluated in this paper).

Industry relevance: The author list is predominantly Amazon Web Services, and the NTP4VC suite is described as an industrial verification-condition benchmark. The infrastructure findings — that a single host lacks Lean capacity for search this wide, and that stateless elaborlation with warm worker pools amortizes import cost — are operational lessons for anyone deploying proof agents at scale. The explicit anti-reward-hacking design (frozen prefixes, axiom allowlists, separately authored specifications) addresses a failure mode that matters directly for production automated reasoning.

Future Directions

• Evaluate other provers on Aegis, and use Aegis for reinforcement learning and multi-teacher on-policy distillation, both explicitly deferred.
• Evaluate the generated mutated variants. Mutation was used to produce additional tasks but is not assessed in this paper.
• Ablate the harness. The authors do not compare against the same model using Lean as a plain tool, nor isolate the contribution of individual components such as parallel tactic probing or context isolation.
• Close the Aegis gap. Roughly half of the sampled statements remain unresolved even for a prover that nearly saturates established benchmarks; which obligation classes resist most, and whether longer budgets or better decomposition close the gap, is open.

Target Audience

Researchers and engineers working on LLM-based theorem proving, program verification, and reinforcement learning from verifiable rewards — particularly those building agentic systems around Lean 4 or evaluating whether a benchmark still measures anything. Readers interested in Rust-to-Lean verification via Aeneas and Charon, or in the practical engineering of scalable proof-search infrastructure, will find the architecture and case studies in the appendix directly useful. The paper assumes comfort with proof assistants and agent architectures; newcomers to the area will get the high-level argument but should expect the methodology to require background reading.

Authors’ abstract

We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier model with no additional training, it proves 669/672 PutnamBench problems and all six IMO 2026 formalizations and resolves 597/600 NTP4VC verification conditions and all 189 VERINA tasks by proof or refutation. Because these benchmarks are close to saturation, we also introduce Aegis, which converts competitive programming problems into much harder verification tasks over real implementations. The pipeline writes safe Rust solutions, translates them into Lean with Aeneas, generates specifications, and labels each frozen statement with a kernel-checked proof or refutation. It produces 2,045 differentially validated Rust-Lean program pairs and 11,533 candidate specifications. Unlike hand-written benchmarks, these tasks carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified sample of 2,000 statements, EasyProver proves 1,054 (52.7%) within a 30-minute budget per statement. The same tasks can also be used to benchmark other provers and as rewards for reinforcement learning.