Scaling Lean Theorem Proving for Real-World Code Verification

Scaling Lean Theorem Proving for Real-World Code Verification. By Debargha Ganguly and eight others, from Amazon Web Services and Case Western Reserve University. Published on the twenty-eighth of October.

Proving theorems in Lean, and verifying code with those proofs, is measured on a handful of standard benchmarks. The authors' own results suggest those benchmarks are close to saturation, which leaves a second problem beside the first: how to keep measuring progress on proofs about real implementations.

The paper answers both. EasyProver is a Lean proving system built from recursive agents with isolated contexts. Aegis is a pipeline that converts competitive programming problems into much harder verification tasks over real implementations.

EasyProver combines four pieces: those recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. It runs on an off-the-shelf frontier model with no additional training.

Aegis works in stages. It writes safe Rust solutions, translates them into Lean with Aeneas, generates specifications, and labels each frozen statement with a kernel-checked proof or refutation. Because the tasks come from real implementations, they carry obligations that hand-written benchmarks do not: fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation.

On existing benchmarks, EasyProver proves six hundred and sixty-nine of six hundred and seventy-two PutnamBench problems, and all six IMO two thousand and twenty-six formalizations. It resolves five hundred and ninety-seven of six hundred NTP4VC verification conditions, and all one hundred and eighty-nine VERINA tasks, by proof or refutation.

Aegis produces two thousand and forty-five differentially validated Rust-Lean program pairs, along with eleven thousand five hundred and thirty-three candidate specifications. On a stratified sample of two thousand statements, with a budget of thirty minutes per statement, EasyProver proves one thousand and fifty-four of them: fifty-two point seven percent. Near-perfect on the old benchmarks, about half on the new one.

The two halves of the paper feed each other. A stronger prover makes the existing tests nearly full marks, so a harder test is built from real code, and that test is not tied to this prover: the same tasks can benchmark other provers and serve as rewards for reinforcement learning.