AI 证明数学定理，靠的不是复杂流程，是接口
大模型证明数学定理，主流做法是给它配一套精心设计的流程：先规划、再拆解、再调度多个专用工具。这篇论文反着来：只给模型一个高效的 Lean 4 接口，让它自己试、看验证器反馈、自我反思，不预设任何结构。结果在多个基准上追平甚至超过那些复杂流程，还解决了 8 个未解猜想。关键发现是：接口效率决定成败，复杂编排是锦上添花。它不是你明天能用上的东西，但对做形式化验证、想让 AI 参与科研数学的人来说，这是个值得记住的信号：先给模型一个好用的执行环境，再谈流程设计。
📄 原文摘要(英文)
While progress in informal mathematics has come largely from scaling the chain-of-thought and agentic reasoning of frontier language models, formal theorem proving has increasingly relied on human-designed workflows around these models, such as planning, decomposition, and orchestrating specialized provers. This raises a bitter-lesson question: can a simple agentic loop that scales test-time compute match these workflows? The answer matters as formal verification must scale to keep up with frontier models producing research mathematics, yet new workflows rarely settle it, as their gains are often confounded with stronger models or more compute. We study this question with h1, a simple harness that gives a model an efficient interface to Lean 4 and keeps it working through verifier feedback and self-reflection, without imposing a decomposition or search structure. h1 reaches state-of-the-art results on PutnamBench, FATE-X, and FormalConjectures100-Solved, settles eight open problems in FormalConjectures, and, at matched models, matches or outperforms specialized workflows such as Goedel-Architect and AlphaProof Nexus, surprisingly showing that a single attempt (pass@1) can often scale to solve open problems. Through ablations and matched-model comparisons with Claude Code and AxProverBase, we find that simplicity alone is not enough: an efficient Lean interface largely determines cost and solve rate. We thus recommend that future work evaluate frontier models with efficient execution feedback before prescribing workflows, at the risk of bitter lessons.