自动定理证明中的苦涩教训：h1 用简单智能体循环匹配专用工作流

arXiv 论文 h1 研究简单智能体循环能否替代人工设计的定理证明工作流。h1 为模型提供高效的 Lean 4 接口，通过验证器反馈和自我反思持续工作，不施加分解或搜索结构，在 PutnamBench、FATE-X 和 FormalConjectures100-Solved 上取得 SOTA，并解决 FormalConjectures 中 8 个开放问题。