Scaling Lean Theorem Proving for Real-World Code Verification

Summary (Overview)

• EASYPROVER: A Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service (INFINILEAN) that nearly saturates current benchmarks using an off-the-shelf frontier model with no additional training.

• Key results on established benchmarks: Proves 669/672 PutnamBench problems (99.6%), all six IMO 2026 formalizations, all twelve Putnam 2025 problems, resolves 597/600 NTP4VC verification conditions (99.5%), all 189 VERINA tasks, and all 77 AlgoVeri tasks.

• AEGIS: A new data environment that converts competitive programming problems into much harder verification tasks over real implementations, producing 2,045 differentially validated Rust–Lean program pairs and 11,533 candidate specifications.

• Performance on AEGIS: EASYPROVER proves only 52.7% (1,054/2,000) of a stratified sample of statements within a 30-minute budget per statement, demonstrating these tasks remain far from saturated.

• Key contribution: The pipeline generates kernel-checked proof or refutation labels for every statement, making the tasks suitable for benchmarking other provers and as rewards for reinforcement learning from verifiable rewards (RLVR).

Introduction and Theoretical Foundation

The paper addresses two fundamental challenges in LLM-based theorem proving:

1. Building effective proving agents: More than a frontier model and proof checker is needed. The agent must decompose goals, find or prove intermediate lemmas, and recover from failed approaches within finite context windows and compute budgets. Verifier feedback is local—Lean reports whether each step elaborates, but the cost of poor decomposition may only become visible many steps later.

2. Evaluating agents on tasks they cannot already solve: Several established formal-reasoning benchmarks are close to saturation (e.g., recent systems report 100% on miniF2F), and existing verified-programming benchmarks are small (hundreds of tasks). Static benchmarks are also exposed to memorization and contamination.

The theoretical foundation draws on:

• Monte Carlo tree search (MCTS) analogy: EASYPROVER's recursive delegation resembles MCTS, but the language model makes expansion decisions from the content of returned results rather than visit counts or rollout-based value estimates.
• Reinforcement learning from verifiable rewards (RLVR): Kernel-checked labels can serve as rewards, since tests give only finite evidence of correctness and can encourage agents to exploit test harnesses.
• Reward hacking prevention: The system blocks weakening theorem statements, leaving sorry, or introducing axioms through frozen statement prefixes and Lean Comparator validation.

Methodology

EASYPROVER Architecture

Problem formulation: Each task fixes a Lean 4 environment Γ and proposition P. The goal is a kernel-checked proof of either P or ¬P. The file prefix up to and including the target theorem signature is frozen; only the proof body can change.

Acceptance criteria: A proof is accepted only if it passes Lean Comparator, which runs lake env lean and #print axioms independently of the language server used during search. Neither the agent's report of success nor a successful local tactic probe counts as acceptance.

Key components:

1. Asynchronous agent runtime: Uses the off-the-shelf Anthropic Fable-5 model with no fine-tuning. Tools cover file operations, Lean proof state inspection, premise retrieval, parallel tactic probing, and recursive delegation through Agent.

2. Recursive, model-directed search: Parents launch children to pursue alternative strategies or auxiliary lemmas. Each child receives a fresh context and private project copy. Children return completed proofs, counterexamples, or partial findings.

3. Context isolation: Decouples total exploration across the search tree from the history any single agent must keep. A child may spend dozens of tool calls deriving a helper lemma and return only the lemma.

4. Parallel tactic probing: Runs several candidate tactics concurrently on the current proof state. Successful tactics are returned while failed probe traces are discarded—e.g., a returned tactic of ~30 tokens may have ~30,000 tokens of probe traces.

5. Resource admission control: Process-wide semaphores cap active sub-agents at 64 and concurrent expensive Lean queries at 16.

6. INFINILEAN (decoupled Lean elaboration): A stateless service backed by a load-balanced pool of Kubernetes replicas. Clients send Lean source over JSON-RPC instead of server-local file paths. Replicas combine a Lean language-server MCP interface, ephemeral workspace, and REPL workers with Mathlib preloaded. Imports take tens of seconds, while elaboration on a warm worker takes ~0.2 s.

AEGIS Pipeline

Implementation corpus: A coding agent writes safe Rust solutions to LeetCode problems. Validated implementations pass:

• Rust reference tests
• CHARON extraction
• AENEAS translation to Lean
• Lean evaluation matching Rust outputs on the same inputs

Of 2,356 problems attempted, 2,045 (86.8%) passed all stages.

Proof obligations in translated programs:

• Operations that may overflow, index out of bounds, or divide by zero return Result α and are sequenced monadically
• Fixed-width values (e.g., Std.U32, Std.I64) expose a mathematical projection .val, with arithmetic and width casts introducing explicit range obligations
• Rust loops become bodies returning ControlFlow with a driver built from the loop combinator
• index_mut operations return the current value with a backward function that rebuilds the updated vector

Specification generation: A specification agent writes elaborating theorem statements with sorry proof bodies, requesting both properties intended to hold (functional correctness, totality, output bounds, edge cases) and intended to fail (missing preconditions, off-by-one bounds). Statements are filtered for duplicates, trivial claims, and elaboration errors.

Optional counterexample screening: Uses Plausible, a property-based testing tool for Lean, to catch drafting errors before proof search.

Empirical Validation / Results

Formal Mathematics Results

EASYPROVER solves 669/672 PutnamBench problems (99.6%), 72 more than the strongest configuration reported by Chung et al. [2026] (597/672).

Code Verification Results

†113 of the 143 CLEVER tasks that translate to Lean 4.32.

EASYPROVER achieves 588 proofs and 9 refutations on NTP4VC.

AEGIS Results

From 11,533 candidate specifications, a sample of 2,000 statements over 1,257 translated programs was drawn, stratified by LeetCode difficulty and specification category. With a 30-minute budget per statement:

• Overall proof rate: 1,054 statements proved (52.7%), 943 unresolved
• By specification type: 84.1% for edge-case specifications down to 31.0% for explicit contracts
• By difficulty: 66.7% on Easy problems down to 37.6% on Hard problems

The same prover that nearly saturates established benchmarks leaves almost half of these statements unresolved.

Theoretical and Practical Implications

For theorem proving systems:

• Demonstrates that an agentic harness around an off-the-shelf model, with no additional training, can achieve state-of-the-art results on multiple benchmarks
• The recursive delegation with context isolation provides a scalable alternative to monolithic context windows
• INFINILEAN's stateless elaboration service decouples proof search from Lean capacity, enabling wide search (hardest proofs used >300 sub-agents in a single run)

For benchmark design:

• AEGIS addresses saturation and contamination problems in existing benchmarks by generating new tasks automatically
• The pipeline needs no expert annotation, so more tasks can be generated with additional compute
• Kernel-checked labels make tasks suitable for RLVR rewards, providing a more robust training signal than test execution

For verification practice:

• The approach handles implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation—the realities of real-world code
• Differential validation provides evidence that the Lean program behaves like the Rust source, while every label is correct for the extracted program regardless of translation quality

Conclusion

EASYPROVER demonstrates that an agentic harness around an off-the-shelf frontier model, with no additional training, can resolve nearly all tasks in several established mathematics and verification benchmarks. AEGIS provides much harder tasks that these benchmarks lack: specifications over mechanically translated safe Rust, with obligations from machine arithmetic, explicit failure, generated loops, casts, and mutation. The same prover proves only 52.7% of a sampled set of these statements, confirming they remain challenging.

The authors note several limitations and future directions:

• No ablation of individual harness components was performed (each configuration requires a full benchmark run)
• No comparison was made against the same model using Lean as a tool without the harness
• Evaluating other provers on AEGIS and using it for reinforcement learning and multi-teacher on-policy distillation is left to future work
• The model's training cutoff is not public, so contamination cannot be ruled out for competition problems (though this does not affect correctness of kernel-checked proofs)