当 Claude、GPT 和 Lean 一起做数学：Knuth 那道难题，正被一个“人机证明共同体”改写

一道老派数学题，突然有了 2026 年的解法

如果把这则新闻拍成电影，开场就已经够戏剧化了：图灵奖得主、《计算机程序设计艺术》作者 Donald Knuth，盯着一个开放问题思考了数周，结果一个 AI 模型 Claude 在大约 1 小时的引导探索里，给出了奇数情形的一类构造。Knuth 震惊到直接把论文命名为《Claude’s Cycles》。

三周之后，剧情没有收束，反而越滚越大。根据 Bo Wang 最新披露的进展，这篇更新后的论文显示，围绕这个 Hamiltonian decomposition（哈密顿分解）问题，已经形成了一整套人机协作链条：Claude 找到奇数 m 的构造；Knuth 继续把基础情形 m=3 的结构数清楚，算出恰好有 11,502 个 Hamiltonian cycles，其中 996 个可以推广到所有奇数 m，再进一步证明这一族里恰好有 760 个有效的“Claude-like”分解；而 Claude 没完成的偶数情形，则被 Ho Boon Suan 博士借助 GPT-5.4 Pro 攻克，给出一个覆盖所有偶数 m≥8 的 14 页证明，并用计算检验一直推到 m=2000。

如果这还不够热闹，后面还有“组合技”：Keston Aquino-Michaels 使用 GPT 与 Claude 协同，借助多智能体工作流找到了奇偶两类更简洁的构造；Kim Morrison 则把 Knuth 关于 Claude 奇数情形构造的证明，形式化到了 Lean 里。换句话说，这不再是某个模型“猜对了一题”，而是一套从发现、证明、简化到形式化验证的数学流水线，第一次如此清晰地摆在了公众面前。

真正值得看见的，不是答案，而是“证明生产方式”变了

很多人看到这类新闻，第一反应往往是：“AI 又抢了数学家的工作？”我倒觉得，这个问题问得有点早，也有点偏。眼下更真实的变化不是替代，而是数学研究的分工正在重排。

传统数学研究里，提出猜想、尝试构造、排除反例、整理证明、同行检验、最后再做形式化验证，往往是一个漫长而线性的过程。它很像手工钟表：精密、优雅，但慢。现在这件事之所以引人注目，是因为我们看到一个并行化的版本出现了：一个模型负责在巨大搜索空间里“乱中取序”，另一个模型擅长把思路展开成更完整的证明文本，人类研究者在关键处判断哪些构造是数学上“像样”的、哪些只是语言模型的幻觉，证明助手再负责把最后的逻辑缝隙一针一线地缝死。

这和过去两年 AI 在编程上的变化很像。最早人们惊叹的是 Copilot 能补全函数；后来行业才意识到，真正改变生产力的不是补全本身，而是从需求拆解、代码生成、测试、重构到 CI 验证的一整条工作链。数学也在走向类似的转折点。过去我们讨论“AI 会不会做数学”，常常盯着某道 IMO 题、某条基准测试榜单；而 Knuth 这件事让人看到，未来更重要的可能不是单次解题能力，而是“研究工作流能力”。

说得直白一点，数学家未来也许不会被一个会做题的模型取代，但可能会被一个会调度多个模型、还能把结果送进 Lean 验证的人机团队甩开半个身位。

为什么偏偏是 Knuth 的题，格外有象征意义

这件事的分量，还来自 Donald Knuth 本人。Knuth 不是普通的学者名字，他几乎是计算机科学里“严谨”二字的人形化身。一个经典段子是，他给读者寄支票奖励勘误；另一个现实是，TeX、METAFONT 这些系统本身就代表着一种近乎执拗的形式美学。这样一位人物公开承认自己被 AI 的结果“震惊”，并把论文直接命名为《Claude’s Cycles》，这本身就是一个时代注脚。

更有意思的是，这并不是 AlphaGo 那类“在封闭规则下打败人类冠军”的熟悉叙事。围棋有明确胜负、状态空间虽大但规则清晰；而数学研究并不是单纯搜索，它包含命题表述、构造灵感、证明压缩、审美判断、可推广性分析，甚至还包括“这条路值不值得继续走”。AI 以前在数学上的亮点，大多集中在辅助计算、自动定理证明、或竞赛题表现。Knuth 这次事件把这些原本分散的能力，第一次压缩到一个非常有故事感的案例里：开放问题、顶级学者、多个模型接力、人类补强、机器形式化验收。

这也是为什么我认为它比又一条“模型数学 benchmark 刷榜”重要得多。榜单常常告诉你模型能不能答对一道题，但不会告诉你它如何成为研究生态的一部分。现在我们终于看到后者了。

热闹背后，也有两个必须追问的问题

当然，兴奋归兴奋，这件事并不意味着“AI 已经真正理解数学”这种大话可以轻易成立。恰恰相反，它提醒我们要更认真地区分三件事：找到构造、写出证明、以及建立可验证、可复用、可推广的数学知识。这三者并不等价。

Claude 在奇数情形上表现惊艳，但偶数情形没完成；GPT-5.4 Pro 补上了这块；之后又有人用双模型协作找到了更简单的构造。这说明什么？说明单个模型的“聪明”还不是重点，重点是不同系统各有所长，而且输出质量高度依赖研究者如何提问、如何筛选、如何组织验证。换句话说，今天最强的未必是某一个 AI，而是会编排 AI 的那个人。

第二个问题是数学信用和署名结构会怎么变。Knuth 给 Claude 的贡献起了名字，这很优雅，但未来若一篇论文的关键构造由 Claude 发现、证明框架由 GPT 组织、反例筛查由程序完成、最终正确性由 Lean 保证，人类作者究竟在署名、贡献陈述和学术评价中占据什么位置？这不是文书细节，而会影响整个学术体系的激励机制。今天学界还可以把它当作新奇个案，明天它可能就会成为投稿、评审与职称体系必须面对的常规场景。

此外，形式化验证的重要性会被进一步抬高。因为模型给出的证明再漂亮，只要还停留在自然语言里，就仍然可能埋着微小但致命的漏洞。Lean 在这里扮演的角色，有点像数学世界的“单元测试 + 编译器 + 审计员”。这次 Kim Morrison 对相关证明的形式化，某种程度上也在告诉大家：未来高价值数学成果，很可能越来越需要“可机器检查”的第二层交付。

从一则趣闻，到一个新研究范式的起点

如果把视角拉高一点，这件事其实与当下 AI 行业的大趋势完全同频。过去一年，多智能体系统、推理模型、工具调用、形式化方法、长上下文协作，几乎是所有头部实验室都在押注的方向。OpenAI、Anthropic、Google DeepMind 讲的虽然是不同产品语言，但底层逻辑很像：单个模型的能力正在接近瓶颈，真正的突破来自系统层面的协作与验证。

而数学，恰好是检验这套逻辑最严苛也最迷人的场景。因为数学不像写营销文案，不能“差不多对”；也不像生成图片，审美可以留有弹性。数学要么成立，要么不成立。也正因如此，一旦 AI 在数学中形成可靠工作流，它对科研、芯片验证、密码学、程序正确性证明等领域的溢出效应会非常大。今天它帮 Knuth 推进图论问题，明天它也许就能帮工程师发现协议漏洞，或者帮编译器团队自动构造形式化证明。

我个人最在意的一点，是这让“研究民主化”第一次显得没那么空洞。过去，能参与前沿数学问题的人，往往需要极强的专业训练和漫长的学术积累。未来，拥有好模型、好工具链、以及足够判断力的研究者，也许能更快进入问题核心。当然，这不会让训练消失，反而会抬高对品味和判断的要求。就像搜索引擎没有让历史学家失业，却让“知道问什么问题”变得更关键。

所以，Knuth 这道题最后是否已经“彻底解决”，在我看来反倒不是最迷人的部分。真正让人有点起鸡皮疙瘩的是：我们亲眼看见了一个新物种的研究现场——人类直觉、语言模型搜索、程序验证、形式化证明，像四种不同乐器，开始能勉强合奏，而且已经不算难听了。