Hugging Face Daily Papers·· 4 天前精选AI 评分58
h1 用简单智能体循环在 Lean 4 上刷新形式化定理证明成绩
h1: A Taste of the Bitter Lesson in Automated Theorem Proving
AI 导读
论文提出 h1，一个只给模型高效 Lean 4 接口、依靠验证器反馈与自我反思持续工作的简单 harness，不预设分解或搜索结构，在 PutnamBench、FATE-X 和 FormalConjectures 100-Solved 上取得当前最优结果，并解决了 FormalConjectures 中的八个开放问题。
推荐理由
论文用匹配模型对比说明，形式化定理证明的成本与求解率主要取决于 Lean 执行接口效率，而非复杂工作流编排。
来源：Hugging Face Daily Papers · huggingface.co