Scaling Lean Theorem Proving for Real-World Code Verification
Debargha Ganguly, Divya Raghunathan, Dejan Jovanović, Soonho Kong, Sam Bayless and colleagues (Amazon Web Services, with Case Western Reserve University) build EasyProver, a Lean proving harness around an off-the-shelf frontier model, and Aegis, a benchmark that turns competitive programming problems into verification tasks over real Rust implementations.
Ask this paper
Harness only. EasyProver uses recursive agents with isolated contexts, asynchronous search, parallel tactic probing and an elastic elaboration service. The underlying model receives no additional training.
Saturated benchmarks. It proves 669 of 672 PutnamBench problems and all six IMO 2026 formalizations, and it resolves 597 of 600 NTP4VC conditions and all 189 VERINA tasks by proof or refutation.
Aegis tasks. The pipeline writes safe Rust, translates it to Lean with Aeneas and generates specifications. It produces 2,045 differentially validated Rust-Lean pairs and 11,533 candidate specifications.
Harder obligations. Aegis statements carry fixed-width arithmetic, explicit failure, generated loops, casts and functionalized mutation. EasyProver proves 1,054 of 2,000 sampled statements (52.7%) within 30 minutes per statement.
Proof size. The 1,054 accepted proof artifacts total 145,646 lines, with a median of 104 lines and a largest artifact of 1,167 lines.
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.