**EasyProver 实现 Lean 定理证明规模化突破，轻松解决 IMO 与 PutnamBench 难题**

_Scaling Lean Theorem Proving for Real-World Code Verification_

> 研究团队推出了基于递归代理的 Lean 证明系统 EasyProver，无需额外训练即可在 30 分钟内解决 669 个 PutnamBench 问题及全部 6 个 IMO 2026 形式化任务。针对接近饱和的基准测试，团队还提出了 Aegis 框架，将编程竞赛题目转化为包含固定宽度算术等复杂约束的验证任务。在 2000 个分层样本中，EasyProver 成功证明了 52.7% 的语句，并生成了大量经过验证的程序对与规范，展示了其在真实代码验证领域的强大潜力。

**来源信息**
- **来源**：HuggingFace Daily Papers（社区热门论文）
- **分类**：论文
- **发布时间**：2026-10-30 08:00（北京时间）
- **原文**：[打开原文](https://huggingface.co/papers/2610.38174)