Hugging Face Daily Papers·· 3 天前精选AI 评分58
EasyProver 与 Aegis：面向真实代码验证的 Lean 定理证明扩展
Scaling Lean Theorem Proving for Real-World Code Verification
AI 导读
论文提出 Lean 证明系统 EasyProver，用递归智能体、异步搜索、并行 tactic 探测和弹性 elaboration 服务，在未额外训练的前沿模型上证明 669/672 道 PutnamBench 题目、全部 6 个 IMO 2026 形式化题目，并解决 597/600 个 NTP4VC 验证条件和全部 189 个 VERINA 任务。
推荐理由
论文给出 EasyProver 在 PutnamBench 与 IMO 上的解题数据，并配套 Aegis 把竞赛题转成更难的代码验证任务。
来源：Hugging Face Daily Papers · huggingface.co