EasyProver nears saturation on Lean verification benchmarks

The team behind EasyProver, a new Lean proving system, reports that an off-the-shelf frontier model with no additional training resolved every one of the 189 tasks in the VERINA benchmark and all six IMO 2026 formalizations, while solving 669 of 672 problems in PutnamBench and 597 of 600 verification conditions in NTP4VC.

"We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service," the paper states. The authors argue that because these existing benchmarks are "close to saturation," they built a harder one.

That new benchmark is Aegis. 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, the tasks "carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation."

On a stratified sample of 2,000 Aegis statements, EasyProver proves 1,054, or 52.7%, within a 30-minute budget per statement. The abstract does not name the frontier model.