AI 解数学题，越简单反而越强
让 AI 证明数学定理，主流做法是给它设计复杂的流程：先规划、再拆解、再调度多个专用工具。这篇反着来：只给模型一个高效的 Lean 4 接口，让它自己试、看验证器报错、再自己改，不预设任何解题结构。结果这个「笨办法」在多个数学竞赛和开放猜想基准上刷新了纪录，还解决了 8 个未解猜想；更反直觉的是，在同样模型下，它比那些精心设计的流程(如 Goedel-Architect、AlphaProof Nexus)更强或持平。研究者发现，关键不是流程多聪明，而是接口多高效——模型能多快拿到验证反馈，直接决定成本和解题率。这提醒我们：在给 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.