执剑人还在——希尔伯特第十问题、马蒂亚谢维奇，与 AI 时代数学家的位置

2026 年 10 月，两件事同时发生。

一件很大：10 月 6 日，OpenAI 在 GitHub 上一次性放出 722 篇由内部模型生成的数学手稿，对应 372 组结果。其中第 004 号结果，是一份 62 页、没有 Lean 形式化验证的预印本，标题是《希尔伯特第十问题：有理数情形》。它声称：不存在算法能判定整系数多项式方程是否有有理数解。消息传得很快，标题很响。圈内人的第一反应却不是“终于”，而是——“谁审？”

一件很小，但更重：人们发现，那个在 1970 年终结希尔伯特第十问题整数版本的人，尤里·马蒂亚谢维奇，还活着，还在审读。

据作者了解，他仍在阅读、判断这类由 AI 生成的数学稿件——用圈内不客气的说法，审“AI Slop”。这不是八卦。这是一个结构性事实：

AI 可以生成无穷多的“定理陈述”，但判断哪些陈述是真的，仍然需要那个知道“不”字有多重的人。

而马蒂亚谢维奇，就是那个写下“不”的人。

这里的“执剑人”不是握按钮的威慑者，而是握着“不”的判断者。

一、126 年，70 年，56 年

1900 年，希尔伯特在巴黎提出第十问题：找一个算法，判定任意整系数多项式方程是否有整数解。

1970 年新年过后第四天，列宁格勒，一个 22 岁的年轻人证明了 Julia Robinson 猜想（她猜想指数增长关系是丢番图的），H10 的否定解就此闭合。他叫尤里·马蒂亚谢维奇。1969 年他才刚从列宁格勒国立大学毕业；1964 年，17 岁，曾获全苏数学奥林匹克冠军。

H10 从提出到被解决，整整七十年。从 1900 年到 2026 年，一百二十六年。从 1970 年到今天，五十六年。

但这个故事最动人的部分，不在“天才少年”的叙事里，而在冷战之中。一个苏联的年轻数学家，接住的是一群美国数学家的接力棒。Davis、Putnam、Robinson 的框架，加上 Matiyasevich 的关键构造，才构成 MRDP（亦写作 DPRM）定理。他在后来的文章《我与 Julia Robinson 的合作》里亲自讲述过这段跨越铁幕的智力接力。

数学的“不”，从来不是一个人说出的；它是一个共同体在几十年里逼近的确定性。

二、2026 年 10 月 6 日：722 篇手稿

这一天发生的事，值得被完整记录。

OpenAI 在 GitHub 上发布了一个仓库（openai/math），包含 722 篇手稿，组织为 372 组结果，涵盖代数、数论、理论计算机科学、数理逻辑、概率论、拓扑学等 17 个领域。据 OpenAI 自述，其内部模型平均每个结果消耗约等于 ChatGPT Pro 连续思考 3 小时的算力，总共尝试了约 4000 个问题。

其中第 004 号结果——《希尔伯特第十问题：有理数情形》——是一份 62 页的预印本，成稿日期 9 月 24 日。它声称：

不存在算法能判定任意整系数多项式是否有有理数零点。变量个数是输入的一部分，不预先限定。

这份预印本没有提供 Lean 形式化验证。 据公开讨论，在 722 篇手稿中，约一半附有机器可验证的 Lean 证书；但 H10 有理数版不在其中。

数学界的反应是即时的、多声部的，也是分裂的。以下是据公开讨论整理的反应：

Peter Sarnak（普林斯顿大学）：他表示在人类验证并理解之前不会称之为“定理”；他还把正在上的一门课改成了研读这个证明的研讨班。

Andrew Sutherland（MIT）：他强调在模型公开、结果可被复现之前，任何关于单个 agent 一次解决问题的说法都应视为未经证实。

Dana Moshkovitz（唯一性博弈猜想专家）：她批评 OpenAI 那篇唯一性博弈预印本写作质量很差，不用 AI 帮忙几乎读不下去。

Terence Tao（菲尔兹奖得主）：他事前曾用“toxic waste”（有毒废料）形容这类成果，事后又调侃为“maybe treated waste”（也许是处理过的废料）。他在 10 月 10 日的演讲中区分了“Math 1.0”（证明稀缺时代）与“Math 2.0”（AI 时代），指出 AI 的使用必须与人类理解的目标对齐。

Hugo Duminil-Copin（菲尔兹奖得主）：他在谈及这次发布时情绪激动，表示自己为这个研究领域的前景感到难过；他担心 AI 公司的目标正在压过数学共同体对理解与传承的坚持。

人类数学协会（Association for Human Mathematics） 在 10 月 7 日发表声明：

“数学家没有要求做这项工作。”“一次发布 700 多个文件，不是学术的展示，而是权力的展示。我们敦促数学家停止与 OpenAI 的合作，回到以人类理解为中心的科学愿景。”

而在更冷静的另一侧，也有人指出：发布完整证明供任何人检查，恰恰是作者所能采取的最暴露的姿态；数学的信誉从来不靠限制谁能说话，而靠检查说了什么。

据公开讨论，质量方面的事实同样冷酷：发布后一天内，3 篇被撤回，14 篇被修订。部分附有 Lean 证书的形式化，证明的其实是比正文声称更弱的结果。OpenAI 方面也承认，发布时并非所有论文都经过内部通读。

这不是“AI 很强”的故事。这是“AI 很快，但‘快’不等于‘对’”的故事。

而“谁来判断它对不对”这个问题，在 722 篇手稿面前，变成了一个物理瓶颈：有能力审稿的数学家极其有限，AI 成果的井喷正在让同行评议体系“消化不良”。

三、他还在那里

马蒂亚谢维奇生于 1947 年 3 月 2 日。2026 年，他 79 岁。他依然在俄罗斯科学院斯捷克洛夫数学研究所圣彼得堡分部从事数理逻辑研究，依然在判断数学的真伪。

据作者了解，他还在阅读、判断由 AI 生成的数学稿件。

在这个时间点上，给出 H10 整数版本否定解的人，依然活着，依然清醒，依然在做判断。这不是历史轶事。这是一个正在发生的结构性事实：AI 可以生成无穷多的“定理陈述”，但判断哪些陈述是真的、哪些只是语法上通顺的“AI Slop”，仍然需要那个知道“不”字有多重的人。

他不需要“威慑”谁。他只需要在场。

他坐在那里审读，本身就是对“AI 将终结数学”这类叙事的沉默反驳。一个在 1970 年就亲手关闭了“全知算法”可能性的人，在 2026 年依然是人类判断力的守门人。这不是因为他比机器“更聪明”，而是因为判断哪条路值得走、哪个证明是活的、哪份稿件只是语法的空转，这项工作在定理的边界之外，不在形式化验证的射程之内。

四、严格证明：全知数学判定器不存在

下面给出精确命题与证明。公众读者可以只看加粗结论；数学读者可以逐行检查。

定义与已知定理

定义 1（算法）。 本文所称算法，指图灵机程序，或任何与之计算能力等价的有限规则系统。算法对给定输入在有限步内停机并输出结果。

定义 2（可计算编码）。 称映射

\gamma:\bigcup_{n\ge 1}\mathbb{Z}[X_1,\dots,X_n]\longrightarrow \Sigma^*

为丢番图命题的可计算编码，若存在算法对任意整系数多项式 $f$ 计算 $\gamma(f)$ ，且 $\gamma(f)$ 是命题

\varphi_f:\quad \exists (x_1,\dots,x_n)\in\mathbb Z^n,\ f(x_1,\dots,x_n)=0

的标准编码。变量个数与全部整系数均包含在编码中。

定义 3（全知数学判定器）。 称算法 $M$ 为全知数学判定器，若对任意一阶算术句子 $\varphi$ 的标准编码 $\ulcorner\varphi\urcorner$ ， $M$ 在有限步内停机，并输出

M(\ulcorner\varphi\urcorner)=\begin{cases}1,&\varphi\text{ 在标准模型 }\mathbb{N}\text{ 中为真},\\0,&\varphi\text{ 在标准模型 }\mathbb{N}\text{ 中为假}.\end{cases}

论题（Church–Turing）。 本文所称“机器”均指定义 1 意义下的算法。非确定性和随机性在标准零错误意义下不扩展可判定集类；若允许不可计算 oracle，则超出本文“机器”定义。

已知定理（MRDP / H10 否定解）。 不存在算法判定任意整系数多项式是否有整数解。等价地，集合

L_{\mathrm{H10}}=\left\{\gamma(f)\ \middle|\ f\in\bigcup_{n\ge1}\mathbb{Z}[X_1,\dots,X_n],\ \exists \mathbf{x}\in\mathbb{Z}^n,\ f(\mathbf{x})=0\right\}

不可判定。

定理与证明

定理（全知数学判定器不存在）。 不存在满足定义 3 的算法 $M$ 。

证明。 反证。假设存在全知数学判定器 $M$ 。

对任意整系数多项式 $f$ （以其标准编码为输入），定义算法 $D$ ：先计算 $\gamma(f)$ ，再输出 $M(\gamma(f))$ 。

由定义 2， $\gamma(f)$ 是命题 $\varphi_f$ 的标准编码；由定义 3， $M$ 在有限步内停机，并正确判定 $\varphi_f$ 的真值。因此 $D$ 在有限步内停机，且

D(f)=1 \iff M(\gamma(f))=1 \iff \varphi_f\text{ 为真} \iff \exists \mathbf{x}\in\mathbb{Z}^n,\ f(\mathbf{x})=0.

于是 $D$ 是判定 $L_{\mathrm{H10}}$ 的算法。这里不需要 $D$ 处理任意字符串 $w$ ，因此不存在“ $\gamma$ 的值域是否可判定”的问题。

但由 MRDP 定理，这样的算法不存在。矛盾。

故反设不成立；不存在全知数学判定器 $M$ 。 $\square$

这个证明没有说明什么

本证明只否定“全知数学判定器”。它不推出：

不存在在广泛认知任务上远超人类的非全知系统；
不存在能解决大量数学问题、生成猜想、辅助证明的强人工智能；
超级智能若存在，必须只依赖“已挖掘的数据结构”。

在本文的算法定义下，超级智能若存在，只能是非全知的：它受可计算性、形式系统边界、计算资源和数据约束，不能保证对任意数学命题终止并给出正确答案。它可以极强，但不能是全数学神谕。

五、孙智伟的 86 个未知数：人类的接力

如果故事停在“722 篇手稿，无人能审”，那它只是一个关于过载的悲剧。但故事没有停在那里。

2026 年 10 月 16 日——OpenAI 发布后整整十天——南京大学数学家孙智伟在预印本平台上发布了一篇论文：《86 unknowns for Hilbert's tenth problem over the rationals》。

这篇论文做了一件非常“人类”的事：它接住了 AI 抛出的断言，然后把它精确化。

OpenAI 的 004 号结果说的是：当变量个数作为输入的一部分、不预先限定时，H10 有理数版不可判定。这是一个关于“存在性”的否定命题——它告诉你“不存在这样的算法”，但没有告诉你需要多少个变量就足够了。

孙智伟的工作明确回应了 004 号结果，并给出了一个具体的上界：86 个未知数。也就是说，他证明了：即使将变量数固定为 86，H10 有理数版仍然不可判定。这不是简单复述；这是把一个“变量数不封顶”的抽象否定，转化为一个“变量数有明确上界”的精确定理。

这个区别至关重要。在 1970 年整数版的 H10 中，Matiyasevich 的关键贡献是给出了把递归可枚举集编码为丢番图方程的构造性方法；孙智伟对有理数版做的事情，在精神上与此相似：他把 AI 的“存在性否定”推进为“变量数有明确上界”的精确定理。

而且，孙智伟的论文明确写道：

“希尔伯特第十问题在整数上已于 1970 年由 Y. Matiyasevich 否定解决。”

接力棒从 1970 年的列宁格勒，经过 2026 年 10 月 6 日 OpenAI 的 722 篇手稿，传到了 2026 年 10 月 16 日南京的一间办公室里。

AI 提出了断言；人类把它变成了可检验的定理。

这不是“人类比 AI 强”的故事。这是“AI 和人类做的是不同的事”的故事。AI 可以在约 3 小时算力内生成一份 62 页的否定性证明；但把这份证明变成一个有明确边界的、可以被数学共同体检验和使用的定理，仍然需要一个人，坐在那里，用他几十年积累的数论直觉，判断哪一步是活的，哪一步是空转。

孙智伟不是执剑人。但他是最早走上前去、把剑捡起来、确认它还能用的人之一。

六、为什么这对数学界是好消息

过去几年，数学家中间有一种低落的情绪：AI 越来越强，我们是不是终将被替代？

这种情绪可以理解，但它建立在一个错误的模型上：把数学想象成一个有限的、等待被穷尽的题库。如果数学是这样一个题库，那么更强的机器终将穷尽它，人的位置就会消失。

不可判定性告诉我们：数学不是这样的题库。

数学不是任何固定形式系统的闭包。对任何一个足够强、递归公理化且一致的形式系统，总存在它无法判定的命题。这不是系统的缺陷，而是数学不能被单一形式系统穷尽的迹象。一个封闭的、可穷尽的系统才是死的。数学永远比任何系统多出一点东西——而那多出的一点，正是选择、解释与判断发生的地方。

不可判定性不是数学的失败，而是数学不能被单一算法一劳永逸地判定的证明。

七、执剑人

在《三体》里，执剑人握着的是一套威慑系统，他的价值在于随时准备按下按钮。马蒂亚谢维奇手里没有按钮。他握着的，是 MRDP 定理本身——一条已经证明的、不可撤销的数学事实：不存在全知判定器。

这条事实在 2026 年的意义，恰恰是对 AI 叙事最冷静的“威慑”：

你可以生成无限多的猜想，但你不能生成一个对一切命题给出正确答案的算法。这是定理，不是意见。

而 2026 年 10 月发生的事，给了这个隐喻一个实证：

25 位菲尔兹奖得主联署声明（2026 年 9 月 11 日，mathandai.org），警告 AI 公司与数学共同体的目标“严重错位”；
人类数学协会 10 月 7 日声明：“这是权力的展示，不是学术的展示”；
Sarnak 把课堂变成研读班，表示在人类理解之前，他不会称之为定理；
孙智伟用十天时间，把 AI 的存在性否定推进为变量数上界 86 的精确定理。

执剑人不是一个人在战斗。执剑人是一个共同体的姿态。

八、数学家的不可替代性在哪里

如果机器不能是全知判定器，那么数学家的核心工作是什么？

不是计算。计算早就交给机器了，而且机器做得更好。

不是检索。检索也交给机器了，而且机器做得更快。

数学家真正在做的事情是：

提出问题。 在无穷多的真命题中，判断哪一个值得证明。“值得”不是一个已经形式化的谓词；它需要共同体的判断。
选择公理。 在集合论的独立性面前，选择哪一条公理不是逻辑推出的，是数学共同体基于结构和美学的判断。
建立新的形式系统。 当旧系统遇到边界时，创造新的语言、新的框架、新的问题域。这不是在系统内部推导，这是在系统之外创造。
判断什么是有意义的。 在证明机器可以验证之后，仍然需要人来判断：这个定理重要吗？这个方向值得走吗？这个结构揭示了什么？

这些工作目前落在形式化与可验证性的边界之外。不是因为它们神秘，而是因为它们涉及选择——在无穷多的可能性中选择一条路。不可判定性保证了不存在单一算法一劳永逸地完成全部判断；它不排除算法族、人机混合系统或新形式系统逐步覆盖更多情形。

数学家的位置，不在于机器永远做不到，而在于数学共同体仍需做出选择、承担解释与判断的责任。

九、写给低落的同行

如果你最近因为 AI 的进展而感到不安，我想说：

你的不安是真实的，但它建立在两个不成立的假设上——数学是一个有限的题库，以及存在一个全知判定器。

后一个假设已被定理否定；而不可判定性也说明，数学不会被任何单一形式系统穷尽。

数学不是题库。数学是活的。它永远比任何系统多出一点东西。那多出的一点，就是你的工作。

不可判定性不是数学的悲观结论，而是数学的乐观结论：它保证了数学不会被单一算法一劳永逸地穷尽，也不会被封闭在一个固定形式系统里；它仍然需要人的判断、人的选择、人的创造。

机器可以验证证明。机器可以搜索证明。机器可以生成证明。

但机器不能替我们决定：什么值得证明。

这就是数学家的位置。它不会被一个全知算法取代，因为数学共同体仍需在形式系统之外做出选择、承担解释与判断的责任。

十、最后

希尔伯特在 1900 年问：是否存在一个算法判定所有丢番图方程？

1970 年，答案是否定的。

2026 年，我们仍然在问同样的问题，只是换了一种形式：机器能不能替我们做数学？

如果“替我们做数学”意味着把判断、选择与理解全部交给机器，答案仍然是否定的。但这次的“不”比上一次更温柔：它不是拒绝机器，而是给数学留出人机共同工作的空间。

那个在 1970 年证明“不存在全知判定器”的人，今天还在审读。

H10 从提出到否定解，等了七十年。从否定解到今天，又过了五十六年。

一百二十六年过去了，数学没有被穷尽，判断力没有被完全自动化。

他还在那里，不是因为机器不够快，而是因为有些判断，仍然需要由人来承担。

他活着，定理就还在被守护。定理还在被守护，数学家就还有位置。

不可判定，是数学还活着的证明。

这不是安慰。这是不可判定性划出的空间。

注释与出处

已确认的事实

MRDP 定理（1970）否定了希尔伯特第十问题整数版本；由此可严格推出不存在判定所有一阶算术命题真值的算法。文中“全知数学判定器”是精确术语，不泛指任何超人类认知系统。
马蒂亚谢维奇生于 1947 年 3 月 2 日，2026 年 79 岁。
2026 年 10 月 6 日，OpenAI 在 GitHub 发布 722 篇数学手稿（372 组结果，17 个领域），其中包含一份声称解决希尔伯特第十问题有理数版本的 62 页预印本（无 Lean 形式化）。
2026 年 10 月 16 日，孙智伟发布《86 unknowns for Hilbert's tenth problem over the rationals》，明确回应 004 号结果，将 H10/ℚ 推进为变量数上界 86 的不可判定性定理。
2026 年 9 月 11 日，25 位菲尔兹奖得主联署发表《人工智能在数学中的严重错位》（mathandai.org）。

据公开讨论

Sarnak、Sutherland、Moshkovitz、Tao、Duminil-Copin 等数学家的反应，据公开讨论整理；其中直接引语已改为间接引语。
发布后一天内 3 篇撤回、14 篇修订；部分 Lean 证书与正文声称存在落差；OpenAI 方面承认发布时并非所有论文都经过内部通读。
人类数学协会（Association for Human Mathematics）2026 年 10 月 7 日声明。

据作者了解

马蒂亚谢维奇仍在阅读、判断由 AI 生成的数学稿件。

说明：本文不判定 004 号预印本的数学正确性，只讨论其验证状态、共同体反应与判断力的位置。

献给马蒂亚谢维奇，献给孙智伟，献给所有仍在提问的人。路漫漫其修远兮，吾将上下而求索。