HuggingFace Daily Papers· Debargha Ganguly, Divya Raghunathan, Dejan Jovanović, Vikash Singh, Soonho Kong, Aaron Tomb, Aman Goel, Ferhat Erata, Sam Bayless·· 3 天前精选AI 评分65
EasyProver：扩展Lean定理证明以验证真实世界代码
Scaling Lean Theorem Proving for Real-World Code Verification
AI 导读
研究团队提出 EasyProver，一个基于递归智能体的 Lean 定理证明系统，无需额外训练即可解决 669/672 个 PutnamBench 问题、全部 6 个 IMO 2026 形式化问题以及 597/600 个 NTP4VC 验证条件。研究还引入 Aegis，将编程竞赛问题转换为更难的验证任务，生成 2,045 个 Rust-Lean 程序对和 11,533 个候选规范。
推荐理由
EasyProver 在多个数学和编程验证基准上接近满分，同时通过 Aegis 生成了更接近真实世界的验证任务，为定理证明提供了新方向。
来源：HuggingFace Daily Papers · arxiv.org