**简单智能体循环即可解决形式化定理证明难题，无需复杂工作流**

_h1: A Taste of the Bitter Lesson in Automated Theorem Proving_

> 研究提出 h1 框架，通过简单的智能体循环结合 Lean 4 高效接口及验证器反馈，无需依赖人工设计的分解或搜索结构，即可在 PutnamBench 等基准上达到最先进结果，并解决多个开放问题。实验表明，在同等模型下，h1 的表现优于 Goedel-Architect 和 AlphaProof Nexus 等专用工作流，证明了单纯扩展测试时计算量即可匹配复杂流程，但同时也指出高效的执行接口是提升求解率的关键。

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