自动定理证明中的苦涩教训（13分钟阅读）

# #34：在自动定理证明中领悟"苦涩的教训" Source: https://essays.johnloeber.com/p/34-bitter-lessoned-in-automated-theorem 2013年，当我开始学习机器学习和数学时，我很快便坚信AI将接管数学研究：未来的伟大证明将由机器来书写。 很长一段时间里，这是一种反主流的观点。当LLM出现时，它们在数学方面表现得非常挣扎。它们勉强能做算术 (https://essays.johnloeber.com/p/16-notes-on-arithmetic-in-gpt-4)。真正的进展直到2024年底推理模型的出现才开始。通过投入更多的测试时算力（test-time compute），模型得以在不犯错的情况下完成数学论证。 今年年初，终局已近在眼前：前沿推理模型同时具备了（1）足以产生有用想法的直觉，以及（2）足以写出一篇短小精悍的全新证明的推理能力。再加上 Lean (https://lean-lang.org/) 的形式化验证，你基本上可以将这个过程循环运行，慢慢"磨"穿整个证明空间。5月，OpenAI 发表 (https://openai.com/index/model-disproves-discrete-geometry-conjecture/) 了平面单位距离问题的证明，为这个新时代打响了发令枪。¹ 我很早就在想做自动定理证明了，时机似乎已经成熟，于是我专门空出几个周末来尝试。 我注意到，这个领域中大多数活跃的人似乎都在做*非形式化*的数学：用 Markdown 或 LaTeX 生成证明文本，然后再用 Lean 进行形式化。我怀疑模型的连贯性不足以在没有形式化的情况下维持正确、长达数十页甚至数百页的论证。因此，我将自己的自动定理证明器完全聚焦在 Lean 上进行工作。 为此，我开发了一个 Lean4 的私有分支。（我发现稳定开源版本对形式化现有定理基本够用，但在高效证明搜索方面有所欠缺。） 我编写了一个自定义的执行框架（harness），用 AI 生成证明策略，并行化不同的方法以及多个子代理之间的交接。（Claude Code/Codex 的默认框架在管理长时间运行的上下文时太容易迷失方向，而且它们处理上下文的方式很容易变得成本过高。） 我将研究聚焦在图论问题上，这似乎最适合自动定理证明，并构建了额外的专用工具，比如一个元程序，用于生成高度可并行的 C++ 程序来搜索针对直接证明策略的对抗性反例。有大量细节需要做对：我的执行框架管理着分布式计算、核心利用率、API 速率限制、缓存内部引理并使它们高度可搜索，等等。仅仅是管理正在进行的证明搜索的巨大上下文/状态 (https://x.com/chi_wang_/status/2096313850870288392) 就是一个很值得思考的难题。我很享受！我为这个项目背后的工程工作感到自豪。 所有这些，都是为"苦涩的教训"做准备。 使用 GPT-5.5 时，我的方法在证明一些新定理方面是有成效的。² 但它很慢。模型仍然会生成大量不正确或不连贯的陈述，而且经常在策略层面碰壁。 当 GPT-5.6 Sol 发布时，效果有了显著提升。模型在生成正确陈述和有效证明策略方面好了很多。³ 我生成了几十万行 Lean 代码，试图解决 57 阶 Moore 图问题 (https://en.wikipedia.org/wiki/Moore_graph) 并证明 Hadwiger 猜想 (https://en.wikipedia.org/wiki/Hadwiger_conjecture_(graph_theory))。⁴ 大约在那个时候，Levent Alpöge 加大了力度，发布了 Jacobian 反例——一个重大成果，但篇幅简短——还没有人开始发表*长篇*的全新成果。迫于紧迫感，我真的很努力了，但最终没能完成 Hadwiger 的证明。每次我接近一个强有力的归约时，它就是无法闭合，我的证明器不得不转向其他策略。⁵ 当 GPT-6 Astra 发布时，能力又迈出了一大步。它令人印象深刻，尤其是基础模型在想出更好的证明策略方面展现出的*直觉*。⁶ 几天后，Navier-Stokes 的存在性与光滑性问题被解决了 (https://openai.com/index/navier-stokes-solution/)，我也停止了自己的努力——与之相比，那些努力已经微不足道。 四周后，OpenAI 用一个未发布的全新前沿模型针对 4,000 个重大问题进行了测试，每个问题平均使用约 3.5 小时的 ChatGPT-Pro-Thinking 等效算力。（我将此解读为*几乎没有*，每个问题最多大概 100 美元的算力。）结果就是 math 仓库 (https://github.com/openai/math)，声称获得了数百个重大成果，其中包括对 Hadwiger 猜想的*证伪*。难怪我怎么都无法让那些归约闭合。 回顾起来，有五件事让我印象深刻： 1. **模型之间疯狂的提升幅度。** 有时候你必须近距离接触一个模型，充分运用其前沿能力的全部深度，才能真正感受到其中的差距。在2026年，把高难度数学问题扔给它们是正确的考验方式：模型的能力足以取得进展并充分展现其智慧，但又不足以轻松解决这些问题，因此每次更新带来的改进都能以完美的分辨率清晰呈现。顺便说一句，既然我们现在已经在积极解决AI出现之前最难的问题，我很想知道 (https://x.com/johnloeber/status/2100988549772558811) 未来我们是否还能保持这种改进的可感知性。也许我们会有某种可无限提升的基准测试，但人们能够亲眼感知模型进步的时代可能已经结束了。 2. **我那些巧妙的工程工作有多么不重要。** 在这个问题上工作很有趣也很有成就感，但苦涩的教训再次被证明至高无上：你为在模型之上构建特化解方案而做的所有精密工作，迟早都会被基础模型的改进碾碎。我想我比大多数人都更早、更深地领悟了这个苦涩的教训，但这仍然以一种切身的方式击中了我。我甚至都懒得把我的任何工作以开源形式发布，因为到现在这已经无关紧要了。也许我的百万行 Lean 定理或那个专用执行框架还有某种残余价值，但当模型很快就能以几分钱的成本一次性完成更优秀的工作时，就连清理代码的这个动作都感觉毫无意义。 3. **变化的突然性。** 我曾预期我们会"缓慢地"——经过数月、也许一两年——进入 AI 数学时代，重大成果一个接一个地被发布出来。我曾预期会有一种征服感、希望、兴奋和合作，随着数学家们逐渐意识到什么已成为可能。但实际发生的是，当我们跨过某个能力阈值的瞬间，神圣的洞见便被毫无浪漫气息的卡车成吨地倒在了我们的门廊上。 4. **人机协作的窗口期有多短暂。** 许多理想主义者一直在想象一个科学及其他领域中人机协作的时代。但今年，我们从数学领域自古以来完全由人类主导，经历了一个人机协作富有成效的夏天（向 Alpöge 先生致敬），然后变成了完全由 AI 主导——⁷ 大概会一直持续到时间尽头。换一种说法，今年我们从 AI 能力无情的指数增长中的绿线跳到了橙线： [](https://substackcdn.com/image/fetch/$s_!_jMe!,f_auto,q_auto:good,fl_progressive:steep/https%3A%2F%2Fsubstack-post-media.s3.amazonaws.com%2Fpublic%2Fimages%2F12a34068-bdb9-4e97-9a37-b2aae8b8b96f_1376x1124.png) 5. **所有这些进展都是在非形式化数学中取得的！** 看起来⁸ 这些证明是用纯文本生成的，然后大约一半在事后进行了形式化，⁹ 这让我大为震撼，因为跟上这些庞大、复杂的论证——涉及繁琐的记号和高度的概念抽象——背后的概念性工作是*极其极其困难的*。我的直觉一直认为，你必须在 Lean 中操作，以便边走边形式化，防止模型偏离方向。他们能够在不进行任何形式化的情况下维持这些论证的逻辑、显然地达到解决方案，然后在事后才进行形式化——就任务的认知难度而言，这一点*让我觉得疯了*。这实际上让我相信，这些模型比表面上看起来要聪明得多得多；这种智慧的尖锐程度可能仍然被严重低估了。 继软件工程师之后，数学界现在是下一个经历 AI 引发的悲伤阶段 (https://x.com/johnloeber/status/2103991581024112837) 的群体：震惊和否认目前是主导情绪。 但对他们来说，究竟失去了什么？在 AI 之前，大多数数学家实际上不会期望自己能证明一个重大定理，他们只会深入理解数学的一小个领域，其余部分都是陌生的抽象。AI 之后，这种情况实际上仍然是相同的，唯一的区别在于，单个数学家做出重大贡献的概率从微乎其微降到了零。 按此标准，当前的数学领域可以分解为两种完全不同的实践： 1. 相对于我们历史上做数学的方式，这个领域基本上变成了一门人文学科 (https://x.com/johnloeber/status/2107982384646050050)——值得学习不是为了职业目的，也不是为了推进其前沿，而是出于教育本身的美德和求知的愉悦。*学习*数学的乐趣——学习别人已经发现的证明——与以前一样，而且更加易于获取。3Blue1Brown 从这个角度评论说，现在是进入数学领域的最佳时机 (https://www.youtube.com/watch?v=LKrwhjOI8Nc)。 2. 就知识的发现而言，未来的收获似乎无限。我们将回答关于宇宙的伟大问题——P=NP、Riemann 猜想、你能想象的每一个问题以及所有你无法想象的问题。¹⁰ 在最根本的层面上，我们将驾驭太阳的力量，将其转化为真理。这些前景既优雅又令人振奋。 坦率地说，人机协作的窗口期如此之短，我曾感到有些失望。但仔细想想，这种失望源于我的竞争心：我曾希望证明一些新定理，利用工具做一些令人印象深刻的事情。但那种想在别人之前做成某事的竞争欲望，归根结底只是一场自我的游戏。当 AI 让我们谦卑并拉平竞争场时，它迫使我们超越那场自我的游戏，专注于理解的美德。这实际上看起来¹¹ 是件好事。 作为数学家，我们失去了竞争并亲身扩展前沿的特权。但我们获得了无限的理解力，并保留了在 AI 为我们发现的无限领域中自由探索的能力。综合来看，我认为这是一笔好交易。而同样的动态很快也会降临到其他所有学科。对一些人来说，适应这个新现实——旧日的某些竞争游戏可能不复存在——或许会令人不安，但我乐观地认为这将带来更好的结果。 #### 关于本篇帖子的讨论 ### 准备好了吗？