Found first: a primary source the press has not covered yet.
Ganguly, Raghunathan, Jovanović and colleagues introduce EasyProver, a Lean proving system that resolves every task on the VERINA benchmark, 597 of 600 NTP4VC verification conditions, and 669 of 672 PutnamBench problems, without any model fine-tuning. The preprint, submitted October 28, also proves all six IMO 2026 formalizations and introduces Aegis, a new benchmark of 2,045 differentially validated Rust-Lean program pairs built from competitive programming solutions.
What the source says
EasyProver runs recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service, against an off-the-shelf frontier model with no additional training. VERINA's 189 tasks are completed by proof or refutation. Aegis was produced by a pipeline that converts competitive programming problems into Rust verification tasks, generating 11,533 candidate specifications validated differentially against Lean; tasks target implementation-level obligations including fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified 2,000-statement sample drawn from Aegis, EasyProver proved 1,054 statements (52.7%) within a 30-minute budget per statement.
Why it matters
Formal software verification has historically required either domain-specific tooling or models fine-tuned on the target proof system. EasyProver shows that inference-time orchestration of a general frontier model can clear established code verification benchmarks without that overhead. The 52.7% figure on Aegis is a first baseline on real Rust programs drawn from competitive programming contests, not constructed examples, which makes it harder to game than synthetic benchmarks. Practitioners evaluating Lean-based verification pipelines now have a zero-training reference system and a stratified Rust benchmark to measure against.