EasyProver proves 1,054 of 2,000 Aegis Lean statements
First merged summary.
EasyProver, with an off-the-shelf model and no extra training, proved 1,054 of 2,000 sampled Aegis statements within 30 minutes.
EasyProver is a Lean proving system of recursive agents with isolated contexts, asynchronous search, parallel tactic probing, and an elastic elaboration service. Using an unnamed off-the-shelf frontier model and no extra training, the authors report it proves 669 of 672 PutnamBench problems, all six IMO 2026 formalizations, 597 of 600 NTP4VC conditions, and all 189 VERINA tasks. Aegis turns competitive-programming problems into harder checks over real Rust code translated to Lean with Aeneas. On a stratified sample of 2,000 statements, EasyProver proves 1,054, or 52.7 percent, within a 30-minute budget. The authors also propose the tasks as reinforcement-learning rewards.
- Aegis yields 2,045 validated Rust-Lean pairs and 11,533 candidate specifications.
- Checks cover fixed-width arithmetic, explicit failure, generated loops, casts, and mutation.
- EasyProver proves 669 of 672 PutnamBench problems and all six IMO 2026 formalizations.
- It proves 597 of 600 NTP4VC conditions and all 189 VERINA tasks.
- Sample result: 1,054 of 2,000 statements proved inside a 30-minute budget.
What each outlet adds
beyond the shared facts- Hugging Face daily papersReports EasyProver’s benchmark totals and the 2,000-statement Aegis sample.
- Products
- EasyProverAegisAeneasLeanLean 4
Coverage
oldest first · one row per article · UTC- · 6d ago
Hugging Face daily papersFirst report
Simple Lean 4 harness h1 matches specialized prover workflows
With matched models, a single attempt plus verifier feedback solved eight open FormalConjectures problems and led three formal benchmarks.
- · 3d ago
EasyProver solves near-saturated Lean benchmarks and half of harder Aegis tasks
On a stratified Aegis sample of 2,000 statements, it proves 1,054 within a 30-minute budget.