AI Papers Reader

Personalized digests of latest AI research

View on GitHub

Agentic Prover Clears Existing Math and Verification Benchmarks but Leaves Half of New Code Tasks Unresolved

Software verification with formal proofs can give guarantees that testing cannot, but writing those proofs is slow and demands rare expertise. A team from Amazon Web Services and Case Western Reserve University reports a system that uses a general-purpose AI model to prove claims about mathematics and programs in Lean, a proof assistant that mechanically checks every step. The researchers also argue that existing benchmarks are close to saturated, and they introduce a harder test set built from real code.

The system, called EASYPROVER, wraps an off-the-shelf frontier model, which the paper identifies as Anthropic’s Fable-5, in an agent harness with no additional training. A parent agent can launch child agents, each with a fresh context and a private copy of the project, to pursue alternative strategies or helper lemmas. Children return only completed proofs, counterexamples, or partial findings, so the parent does not inherit their failed attempts. A separate tactic prober tests candidate proof steps in parallel. In one example the authors give, the returned step was about 30 tokens, while the discarded probe traces totaled about 30,000. A stateless elaboration service, INFINILEAN, lets many machines check proofs at once. A proof counts only if it passes an independent checker that rejects placeholders and unapproved axioms.

On established benchmarks, the authors report 669 of 672 PutnamBench problems proved (99.6%), compared with 597 of 672 (88.8%) for the strongest configuration reported by Chung et al., which used natural-language guidance. The system also handled all six IMO 2026 formalizations and all twelve Putnam 2025 problems. On NTP4VC, a code-verification suite, it resolved 597 of 600 conditions (99.5%) by proof or refutation, 588 of them proofs and nine refutations. Earlier specialized provers proved between 2.17% and 3.00% on that suite, but that figure measures proofs alone, so it is not directly comparable. All 189 VERINA tasks and 77 AlgoVeri tasks were resolved, and 113 of 143 CLEVER tasks (79.0%) that could be translated to the team’s Lean version were resolved.

To create harder tests, the team built AEGIS, which generates verification tasks from LeetCode-style problems. An agent writes safe Rust solutions, which are translated into Lean. A separate agent writes candidate specifications, and each is frozen before the prover sees it. Fixed-width arithmetic creates an example of added difficulty. Operations that might overflow return an explicit result type, so proving totality can require showing that a failure branch is unreachable, even when the bounds “do not affect the mathematical answer,” as the authors put it. Of 11,533 candidate specifications, the team sampled 2,000. Within a 30-minute budget per statement, EASYPROVER proved 1,054 (52.7%) and left 943 unresolved. The proof rate ranged from 84.1% for edge-case specifications to 31.0% for explicit contracts.

The paper has clear limits. The model’s training cutoff is not public, so the authors cannot rule out that some competition solutions appeared in its training data, though every accepted proof is still machine-checked. The team did not ablate individual harness components. The hardest proofs used more than 300 sub-agents, and cost rises steeply with time, according to the authors’ analysis. AEGIS has not yet been run on other provers, and its mutation-based variants were not evaluated. The unresolved half of AEGIS may reflect the time budget as much as intrinsic difficulty.

The work suggests that agentic search, rather than specialized training alone, can clear current formal benchmarks, and that tasks generated from real implementations can restore headroom. Because each label is a kernel-checked result, the authors also propose using such tasks as reinforcement-learning rewards, though they have not tested that use.