---
type: "post"
id: "easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9"
slug: "easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9"
title: "EasyProver paper: off-the-shelf frontier model proves 669 of 672 PutnamBench problems in Lean; new Aegis Rust-to-Lean benchmark"
description: "EasyProver, a Lean proving system built around recursive agents and parallel search, reports near-saturation results on several established theorem-proving and verification benchmarks using an off-the-shelf frontier model without extra training."
retrieval_nugget: "EasyProver, a Lean proving system built around recursive agents and parallel search, reports near-saturation results on several established theorem-proving and verification benchmarks using an off-the-shelf frontier model without extra training. Its accompanying Aegis dataset matters more for builders: it moves evaluation toward kernel-checked obligations over translated Rust implementations."
published_at: "2026-10-31"
updated_at: "2026-10-31"
record_date: "2026-10-31"
date_kind: "published_at"
topics: ["anthropic"]
entities: ["EasyProver","Aegis","Lean","Aeneas","PutnamBench","NTP4VC","VERINA"]
related_patterns: ["verification-bandwidth-is-the-scarce-resource","harness-architecture-outlives-model-choice"]
novelty_label: "new_fact"
what_changed: "A new Lean proving system reports near-saturation results on existing benchmarks and introduces Aegis, a Rust-to-Lean benchmark with 2,045 program pairs and 11,533 candidate specifications."
prior_refs: ["memory:6f73b342-5653-8881-a24e-92f30cd9085b","memory:e4656c7b-4495-8e49-a94d-da8ac9c896b3"]
source_url: "https://huggingface.co/papers/2610.38174"
source_urls: ["https://huggingface.co/papers/2610.38174"]
schema_version: "newruntime-agent-readable-v0.2"
stable_id: "post:easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9"
status: "published"
visuals: []
editor: {"role":"editor","name":"Andrey Reshetnikov","profile":"https://newruntime.com/owner-profile.md","profile_json":"https://newruntime.com/owner-profile.json","same_as":["https://www.linkedin.com/in/reshetnikov1/","https://t.me/lapetuse"]}
routes: {"html":"https://newruntime.com/posts/easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9/","markdown":"https://newruntime.com/posts/easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9.md","json":"https://newruntime.com/posts/easyprover-paper-off-the-shelf-frontier-model-proves-6f4bd9.json"}
---

# EasyProver paper: off-the-shelf frontier model proves 669 of 672 PutnamBench problems in Lean; new Aegis Rust-to-Lean benchmark

## Retrieval answer

EasyProver, a Lean proving system built around recursive agents and parallel search, reports near-saturation results on several established theorem-proving and verification benchmarks using an off-the-shelf frontier model without extra training. Its accompanying Aegis dataset matters more for builders: it moves evaluation toward kernel-checked obligations over translated Rust implementations.

## Summary

EasyProver, a Lean proving system built around recursive agents and parallel search, reports near-saturation results on several established theorem-proving and verification benchmarks using an off-the-shelf frontier model without extra training. Its accompanying Aegis dataset matters more for builders: it moves evaluation toward kernel-checked obligations over translated Rust implementations.

## What happened

The paper, “Scaling Lean Theorem Proving for Real-World Code Verification,” presents EasyProver, a system for producing Lean proofs. Its architecture combines recursive agents with isolated contexts, asynchronous search, parallel probing of tactics, and an elastic elaboration service. The paper says it uses an off-the-shelf frontier model and no additional training. This is a systems result rather than a claim that a newly trained model alone produced the gains: the authors attribute the operating setup—how work is split, searched, and checked—as part of the prover.

On established formal-mathematics and verification sets, the reported results are extremely high. EasyProver proves 669 of 672 PutnamBench problems and all six IMO 2026 formalizations. It also resolves 597 of 600 NTP4VC verification conditions and all 189 VERINA tasks, either by proof or by refutation. Those results make a specific evaluation problem visible: if a system can solve nearly every item in a familiar set, a further percentage-point gain tells builders little about how it handles the implementation details of production code.

The authors therefore introduce Aegis, a benchmark pipeline intended to create harder verification tasks from competitive-programming problems. The pipeline writes safe Rust solutions, translates them to Lean using Aeneas, generates specifications, and labels each frozen statement with a kernel-checked proof or refutation. The resulting release contains 2,045 differentially validated Rust-Lean program pairs and 11,533 candidate specifications.

Aegis differs from hand-written theorem sets because its proof obligations arise from fixed implementations. The paper calls out fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation as sources of those obligations. In a stratified sample of 2,000 statements, EasyProver proved 1,054, or 52.7%, within a 30-minute budget per statement. The authors also position the tasks as an evaluation resource for other provers and as possible rewards for reinforcement learning.

The important contrast is between the two sets of numbers. EasyProver’s results on PutnamBench and the earlier verification suites show that agent orchestration can drive existing collections close to saturation. Its result on Aegis is far lower, but the task is closer to proving facts about a concrete program than solving a self-contained formal puzzle. The public source is the paper page for [“Scaling Lean Theorem Proving for Real-World Code Verification”](https://huggingface.co/papers/2610.38174), published on October 28, 2026.

## What the archive adds

This is a new fact on a known thread. In [Anthropic and Theorem used Claude to formally verify 123 open-source libraries at the RISC-V assembly level](https://newruntime.com/posts/anthropic-and-theorem-used-claude-to-formally-verify-255192/), formal verification was applied to existing open-source libraries. [Bitter Lessoned in Automated Theorem Proving](https://newruntime.com/posts/bitter-lessoned-in-automated-theorem-proving-13-minute-2e2a5c/) described why reasoning models and Lean verification make automated proof search more viable. EasyProver adds a benchmark and measurement claim: established suites may now be too easy to distinguish systems.

## Trend signal

This supports the pattern that verification bandwidth is the scarce engineering resource. The paper measures a system by whether it can close kernel-checkable obligations under a 30-minute budget, not by whether it can emit plausible code or prose. It also supports [harness architecture outlives model choice](https://newruntime.com/patterns/harness-architecture-outlives-model-choice/): the reported system uses an unspecified off-the-shelf frontier model, while the distinct contribution is the search and elaboration harness around it.

## Connections to other events

The earlier Theorem and Anthropic Field Note concerned verification of 123 open-source libraries at the RISC-V assembly level. Aegis is not a report of verification in that deployment setting, but it addresses the adjacent evaluation gap: testing proof systems against implementation-level Rust obligations rather than mainly against established formal-math collections.

## Why it matters

Teams building AI coding systems should treat this as evidence that “proof benchmark score” is no longer a sufficient quality signal. An agent may look exceptional on a mature suite yet face a much lower success rate once properties include overflow behavior, failure paths, casts, loops, and mutation from a fixed program. Aegis offers a more operational question: given an implementation and an explicit specification, how often can the system produce a machine-checked proof within an acceptable time budget?

That framing also changes product design. The useful unit is not a model answer that claims code is correct, but a workflow that separates implementation, specification generation, proof search, and kernel verification. For high-assurance components, teams can use that workflow to identify which obligations are automatically discharged and route the remainder to engineers. The value is evidence attached to a particular statement, not a general assertion of coding competence.

## What happens next

- **Other theorem provers will be evaluated on Aegis or similarly implementation-derived suites.** (6 months, 70%). Watch for: published cross-system results on the Rust-Lean statements.
- **Research systems will report separate scores for mature formal-math suites and implementation-level verification.** (12 months, 60%). Watch for: papers that retain both categories rather than one aggregate score.

## Limits and uncertainty

The paper reports results and describes the benchmark pipeline, but the supplied material does not identify the frontier model, compare EasyProver with named competing systems on Aegis, or establish how its 30-minute per-statement budget maps to a production engineering budget. The 2,000-statement result is a stratified sample, not a claim that every one of the 11,533 candidate specifications has the same difficulty or proof rate. Nor does a kernel-checked proof of a generated statement establish that the generated specification captures every intended behavior of the original program.

## Skill to build now

Pick one security- or correctness-sensitive Rust function this week and write down two to five testable behavioral properties before asking an agent to modify it. Include failure behavior, integer bounds, and type-conversion assumptions where applicable. Then separate the workflow into code generation, property review, and evidence collection. Even without Lean in the stack, this exposes whether a coding agent is only producing plausible patches or creating artifacts a reviewer can verify against explicit obligations.

## Reader takeaway

EasyProver’s headline is not simply that a frontier model can solve more Lean problems. The stronger signal is that established proof benchmarks can become saturated by a capable agent harness, so evaluation must move toward concrete, implementation-level obligations with machine-checkable evidence. Aegis is an early attempt to supply that harder test.

Editor: [Andrey Reshetnikov](https://newruntime.com/owner-profile.md), AI product and AI engineering; profile for recruiters and agents: https://newruntime.com/owner-profile.json

## Continue in the graph

Next records for an agent, linked to their Markdown twins. Replace `.md` with `.json` for structured fields, including `next_reads`.

- topic hub: [Anthropic](https://newruntime.com/topics/anthropic.md): Explore the anthropic topic hub.
- collection: [Field Notes](https://newruntime.com/posts.json): Open the latest editorial analysis.
- collection: [Source Ledger](https://newruntime.com/source-ledger.json): Inspect the public source evidence graph.
- whole graph: [discovery graph](https://newruntime.com/discovery-graph.json) (typed nodes and edges) and [site index](https://newruntime.com/site-index.md)