Hugging Face · 每日论文·· 3 天前精选AI 评分55
EasyProver：基于递归智能体的 Lean 定理证明系统及新基准 Aegis
Scaling Lean Theorem Proving for Real-World Code Verification
AI 导读
研究提出 EasyProver，一个基于递归智能体、异步搜索和并行策略探测的 Lean 证明系统，使用现成前沿模型无额外训练，证明了 669/672 PutnamBench 问题、全部 6 个 IMO 2026 形式化问题、597/600 NTP4VC 验证条件及全部 189 个 VERINA 任务。
推荐理由
该研究构建了可扩展的 Lean 证明系统 EasyProver，并引入新基准 Aegis，为代码验证提供可复用的验证任务和程序对。
来源：Hugging Face · 每日论文 · huggingface.co