Scaling Lean Theorem Proving for Real-World Code Verification

Hugging Face Daily Papers Papers
theorem-proving lean formal-verification reinforcement-learning agents benchmarking rust

Summary

The paper presents EasyProver, a Lean proving system using recursive agents and asynchronous search that near-saturates PutnamBench and IMO benchmarks with an off-the-shelf frontier model, plus Aegis, a pipeline converting competitive programming into harder real-world Rust-to-Lean verification tasks for benchmarking and RL.

We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier model with no additional training, it proves 669/672 PutnamBench problems and all six IMO 2026 formalizations and resolves 597/600 NTP4VC verification conditions and all 189 VERINA tasks by proof or refutation. Because these benchmarks are close to saturation, we also introduce Aegis, which converts competitive programming problems into much harder verification tasks over real implementations. 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, these tasks carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified sample of 2,000 statements, EasyProver proves 1,054 (52.7%) within a 30-minute budget per statement. The same tasks can also be used to benchmark other provers and as rewards for reinforcement learning.
Original Article
View Cached Full Text

Cached at: 10/30/26, 03:13 PM

Paper page - Scaling Lean Theorem Proving for Real-World Code Verification

Source: https://huggingface.co/papers/2610.38174

Abstract

EasyProver is a Lean proving system using recursive agents and asynchronous search that solves nearly all Putnam and IMO benchmark problems, while Aegis generates harder verification tasks from competitive programming to benchmark provers and support reinforcement learning.

We present EasyProver, a Lean proving system built from recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an off-the-shelf frontier model with no additional training, it proves 669/672 PutnamBench problems and all six IMO 2026 formalizations and resolves 597/600 NTP4VC verification conditions and all 189 VERINA tasks by proof or refutation. Because these benchmarks are close to saturation, we also introduce Aegis, which converts competitive programming problems into much harder verification tasks over real implementations. 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, these tasks carry implementation-level obligations from fixed-width arithmetic, explicit failure, generated loops, casts, and functionalized mutation. On a stratified sample of 2,000 statements, EasyProver proves 1,054 (52.7%) within a 30-minute budget per statement. The same tasks can also be used to benchmark other provers and as rewards forreinforcement learning.

View arXiv pageView PDFAdd to collection

Get this paper in your agent:

hf papers read 2610\.38174

Don’t have the latest CLI?curl \-LsSf https://hf\.co/cli/install\.sh \| bash

Models citing this paper0

No model linking this paper

Cite arxiv.org/abs/2610.38174 in a model README.md to link it from this page.

Datasets citing this paper0

No dataset linking this paper

Cite arxiv.org/abs/2610.38174 in a dataset README.md to link it from this page.

Spaces citing this paper0

No Space linking this paper

Cite arxiv.org/abs/2610.38174 in a Space README.md to link it from this page.

Collections including this paper0

No Collection including this paper

Add this paper to acollectionto link it from this page.

Similar Articles

A Rust-to-Lean verification pipeline with AI provers: An experience report

Lobsters Hottest

This paper presents an experience report on a verification pipeline that uses AI provers (Aristotle and Aleph) alongside symbolic extraction tools and formal cryptographic libraries to produce machine-checked correctness proofs for Rust cryptographic code in Lean 4, with case studies from the Ethereum Foundation's zkEVM project.

OpenProver: Agentic and Interactive Theorem Proving with Lean 4

arXiv cs.AI

OpenProver is an open-source system for LLM-driven automated theorem proving using Lean 4, featuring a Planner-Worker-Verifier architecture and both autonomous and interactive modes. It enables reproducible evaluation and human-AI synergy in mathematical proof search.

Pythagoras-Prover: Advancing Efficient Formal Proving via Augmented Lean Formalisation

arXiv cs.AI

Pythagoras-Prover is a compute-efficient family of Lean theorem provers that achieves strong performance using curriculum supervised fine-tuning and a novel Augmented Lean Formalisation technique. The 4B model surpasses DeepSeek-Prover-V2-671B at pass@32 on MiniF2F-Test, and the 32B model sets a new state-of-the-art among open-source provers.

Discover and Prove: An Open-source Agentic Framework for Hard Mode Automated Theorem Proving in Lean 4

arXiv cs.CL

This paper introduces Discover and Prove (DAP), an open-source agentic framework for automated theorem proving in Lean 4 that tackles 'Hard Mode' problems where the answer must be discovered independently before formal proof construction. The work releases new Hard Mode benchmark variants and achieves state-of-the-art results while revealing a significant gap between LLM answer accuracy (>80%) and formal prover success (<10%).