--- title: "已验证不等于有发现：证明检查器无法告诉你的事" url: https://wakenex.com/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/ language: zh-CN type: article section: "系统研究" published: 2026-10-27 author: "WAKENEX" id: "article:verified-is-not-discovered-what-a-proof-checker-cant-tell" alternate_language: https://wakenex.com/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/index.md license: "© WAKENEX。可引用与摘要，请注明出处并附原文链接。" cite_as: "WAKENEX. \"Verified Is Not Discovered: What a Proof-Checker Can't Tell You.\" wakenex.com, 2026-10-27. https://wakenex.com/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/" --- # 已验证不等于有发现：证明检查器无法告诉你的事 > OpenAI 称它的 AI 推翻了一个著名猜想、又证明了另外两个，论证也通过了一个名为 Lean 的证明辅助器的检查——但一次通过的检查，所回答的问题远比那些标题假定的要狭窄。 **一句话判断：** 机器验证的证明只是转移了信任问题，并没有消除它。 **WAKENEX 概念：** [反馈分工：不要用一种指标替代其他问题的答案](https://wakenex.com/zh/concepts/match-the-feedback-to-the-question/) ![明亮的阳光大厅里，一只手握着一台巨大的机械印章，把一枚发光的印记盖在一摞空白纸张上，而刚被盖章的那张纸正向上化作雾气。](https://wakenex.com/assets/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/cover-1600.jpg?v=afff8cee35) *图片：WAKENEX* 2026 年 10 月 26 日，OpenAI 表示，一个内部模型做成了一件若按字面理解、将跻身十年来最重要科学事件之列的事。它推翻了指数时间假设（Exponential Time Hypothesis）——计算复杂性理论的一块基石。它在所有维度上证明了局部光滑猜想（local smoothing conjecture），而该公司称这同时解决了 Kakeya 猜想与 Stein 限制性猜想。它还为若干关键量子场论给出了存在性证明，包括 QCD 与杨–米尔斯（Yang-Mills）——那类悬赏百万美元的问题。三项论证中有两项由一个名为 Lean 的证明辅助器逐行检查，并上传到一个公开仓库，任何人都可以查验。 最自然的结论——机器做了研究，而机器的成果已经过验证——几乎是每一条标题都得出的那个。它也恰恰是 Lean 检查无法支撑的那个论断。证明辅助器只认证一件事：一串形式化步骤确实能从它被给定的公理推出。至于那条链条顶端的命题是不是那个著名猜想、结果是不是新的、以及在物理这一例里那些符号是否描述了真实世界，它一概不说。验证收窄了你必须信任的东西，却没有把一个你可以不再去想的发现交到你手上。 ## Lean 这类证明辅助器究竟认证了什么 Lean 属于一类建立在一个古老想法之上的工具，这个想法有时被称作 de Bruijn 准则：与其信任一长串巧妙的论证，不如把它拆成细小、笨拙的步骤，让一个微小而可信的程序，对照一组固定的公理逐一重新核对。如果程序接受了这份证明，你就得到了数学所能提供的、近乎最高的确定性——这个形式化定理确实能从形式化规则推出。相比 AI 系统迄今在数学上拿出的大多数东西，这是一个实打实的进步，那些东西往往是流畅、却经不起推敲、一查就散架的自然语言论证。被 Lean 接受的证明不会那样散架。它消除了一个形式化论证最常见的死法——一个所有人（包括作者）都忽略了的隐藏逻辑漏洞——前提是你同时信任内核本身的代码、并且它起步所依赖的公理是自洽的、而不是悄悄自相矛盾的。 所以，当 OpenAI 在 10 月 17 日把它的计算机科学结果、10 月 19 日把它的数学结果都做了形式化并放上 GitHub 时，它做成了一件真实且可核验的事。审阅者不必听信任何人说这些论证是自洽的。内核已经说了，它们是。 但要注意这句话里包含了什么、又漏掉了什么。内核验证的是一个特定的形式化定理——叫它 T——可被推出。T 是一个人写下的一串符号，用来替代一个非形式化的猜想——叫它 C——后者活在教科书里、活在那些为之耗费职业生涯的人脑中。内核从不检查「T 的意思就是 C」。它做不到。「意思是」不是一种形式关系；它是一个关于翻译是否忠实的人类判断。 ## 检查器只读了翻译的一面 这就是「已验证」这个词悄悄完成的那一步腾挪。任何对一个著名结果的形式化证明，都依赖一个证明辅助器无法审核的翻译步骤：总得有人写下那个形式化命题，也总得有人认定它说的就是那个猜想说的。如果翻译忠实，Lean 检查就接近一锤定音。如果翻译悄悄削弱了论断、添了一个方便的前提、或者把某个关键对象定义成让证明得以走通的样子，内核照样打印出同样的绿色结果。证明是有效的，只是那个定理并不是你以为的那个。 这不是杞人忧天。今年秋天，Mikołaj 与 Krzysztof Sienicki 对 OpenAI 早前由 AI 生成的证明所做的一次人工审计，划出的正是这条线：形式化验证能确认一个证明遵守了它的形式规则，却不保证这个证明在数学上是成立的、或是新颖的。一个结果可以是形式上可验证的，同时仍带着未言明的假设、相对于本意命题的逻辑缺口、或者根本谈不上任何真正的洞见。他们论证道：验证是必要的，却远远不够；数学内容仍然得由数学家来判断。 换句话说，检查器以完美的细致读了翻译的一面，而从不看另一面。论断越难、越出人意料，翻译要承载的分量就越重——而一个绿色对勾能告诉你的，就越少。 ![一束光在检视一块齐整的晶体石板，而一座未点亮的桥通向远处的一座山；英文标题下方是一行中文](https://wakenex.com/assets/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/fig1-1600.jpg?v=825db0b902) *图片：WAKENEX* ## OpenAI 公布了什么，又扣下了什么 这家公司自己的做法，是它清楚「检查不等于论断」的最好证据。数学与计算机科学的形式化公布了，物理的没有。OpenAI 称它在 10 月 16 日用 Lean 形式化了杨–米尔斯结果，然后——没有把它贴出来——扣下了相关材料，交给一个人类小组，成员包括 David Gross、Michael Douglas、Arthur Jaffe、Igor Klebanov 与 Nikita Nekrasov。杨–米尔斯问题的官方表述，起初正是 Jaffe 参与写下的。如果一份 Lean 形式化就能了结此事，那个小组几乎无事可做。把最大胆的论断交给人类专家、而不是让一份公开的 Lean 文件独自站台，这个决定非常说明 OpenAI 认为这项检查究竟能了结多少。其中有些保留或许出于策略——一家公司并不必把一切都公开——但最直白的解读，也被公告的措辞所印证，是：一份物理存在性证明的形式化，可信程度顶多等于它起步所用的那些定义，而判断那些定义是否抓住了真实的物理，是物理学家的活，不是内核的。 公告里的措辞也指向同一处。OpenAI 把模型的产出称为「仍需转化为科学理解的原始研究数据」，并承认它对「最先让哪些专家参与」的选择「不可避免地塑造了谁最先被卷入，并制造了一种信息的不对称」。这是一家公司在描述一份交给人类去完成的未竟之作——而不是一个已成定局的发现。 三项论断没有一项经过同行评审。产出它们的模型是内部的、未公开的，所以外人无法复现结果、也无法探查它在哪里脆弱。就连那条标题也比听上去要克制：对指数时间假设的推翻，附带的算法运行时间大约是二的「n 除以根号 log n」次方——次指数级，但仍远慢于任何多项式，所以它把 P 与 NP 的问题原封不动地留在了原处。而那个仓库里已经有了一个警示性的例子。10 月 7 日，也就是一次更早的大规模公布之后的第二天，一份 AI 写就的手稿里的一个符号错误使一段论证失效，三篇论文被撤回。Lean 能抓住活在形式化证明内部的错误，却抓不住活在它之前那一步里的错误——在那一步，是人把一个想法变成了符号。 ![一张数据卡，对照 Lean 检查了结了什么与没能了结什么；英文标题下方有一行中文](https://wakenex.com/assets/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/fig2-1600.jpg?v=1df6641af2) *Chart: WAKENEX · Source: the company's Oct 26 announcement; datastudios.org; unite.ai; arXiv:2608.14673 · as of 2026-10-27* ## 认为这次确实不一样的最有力理由 这个公允的反方值得一听，因为它很有力。一份 Lean 证明绝非无足轻重。它消除了那个让以往每一波 AI 数学都出过丑的失败模式，而且是公开地做到的，以一种专家可以攻击的形式。做检查的人并不是市场部；在好几例里，他们就是提出这些猜想的研究者本人。Russell Impagliazzo 与 Ramamohan Paturi——二十多年前提出指数时间假设的三人中的两位——正与 MIT 的 Ryan Williams 一起审阅对它的所谓推翻。这些是对的裁判，而形式化此刻就握在他们手里。如果他们回来说，形式化命题是忠实的翻译、证明是新颖且正确的，那条标题就算挣得了。 不过，这恰恰是要点，而非对它的反驳。这里的论点并不是说那些结果是错的。它们中的任何一个都可能是一次真正的进展；数学界会告诉我们。论点关乎的是：究竟是谁在做那个「确认」。在这个好结局的每一个版本里，是人类的审阅在为这项发现背书，而 Lean 检查是一个有力却次要的证人。绿色结果把证明送进了房间。是房间里的人在决定一个翻译是否忠实、一段论证是否新颖。那份劳动无法被形式化，这恰恰是它至今没有被形式化的原因。 这个反方还有一个更锋利的版本值得直说，因为它正好戳在我们自己的框架上。我们一直把翻译这一步——形式化命题与著名猜想之间的缝隙——当作信任如今所在之处。但对这么著名的猜想来说，形式化命题并不晦涩。指数时间假设与杨–米尔斯存在性问题都有规范的、经过公开论证的表述，专家可以读它，并在一个下午之内拿它与一份形式化作对照。在猜想是标准表述的地方，忠实性这个问题既狭窄又能被很快了结，而一份 Lean 检查确实接近于了结这场论证。这就是我们这个观点诚实的边界。对这几项具体结果而言，残留的缝隙与其说在于命题是否忠实，不如说在于这份证明是不是一次真正的发现——新的数学——而不是把已知招式做了一次漂亮的形式化拼装。忠实性，专家一个下午就能查。新颖性与重要性，他们查不了，而没有任何证明辅助器曾被造出来去尝试这件事。 ## 验证转移了信任，并没有消除它 剥掉这场景观，剩下一个简单的结构。证明辅助器把「这段论证内部是否正确？」这个问题——它过去会吞掉审稿人的大半时间——转换成了两个它碰不到的问题：「这个形式化命题真的是那个猜想吗？」以及「这是不是一次真正的发现？」两者都是关于意义与新颖的判断，而两者都仍然归人类所有。验证没有废除信任。它把信任挪了地方——从那条长长的证明步骤之链，挪到了顶端那段不起眼的翻译，以及其下那个更难的「值不值得」的问题。 这种挪移是实打实的进步。把你的信任从一千个脆弱的步骤挪到一个被反复推敲过的定义上，是一个更好的立足点。但一个更好的立足点，并不等于再也不必站在任何地方；而那些标题兜售的是后一件事，与此同时 OpenAI 在它自己的仓库里、用它自己谨慎的句子，做的是前一件事。 ## 如果你用 AI 来做自己的工作，这意味着什么 这其实并不是一个关于千禧年大奖难题的故事。它是与强大 AI 协作的日常样貌，被放大到了最戏剧化的形态。你让一个系统做点东西，它递给你一个通过了某种检查的产物：测试是绿的、代码能编译、证明被接受、linter 干净。诱惑在于把「通过了检查」读成「做完了」。这些检查的强度天差地别——一份 Lean 内核证明是相对于其公理的完整演绎保证，而一套通过的测试只是少数几个被抽样的例子——可这个教训跨过了这种差别依然成立，因为哪怕是最强的检查，也对同样的三件事保持沉默。一次检查永远只告诉你：这个产物与你给它的那份规格是内部自洽的。至于规格本身对不对、产出是新颖的还是只是把已有之物流畅地重排了一遍、以及这东西到底值不值得做，它一概不说。这正是 Lean 内核回答不了的同样三个问题，只不过换上了工作服。 可行的做法，是守住人类判断那一步，并且拒绝让「已验证」顶替「正确且值得做」。一个绿色对勾是你判断的一个输入，不是它的替代品。这周的小检验不花一分钱：挑一个你曾因为「它通过了」就说「做完了」的 AI 产物，用一句话写下这项检查实际上没有验证的那一件事。如果你说不出来，那你还没审完——你只是看着机器审了它自己。 ![一个人坐在桌前，屏幕上亮着一个鲜绿的对勾，而键盘旁放着一盏未点亮、标着那个真正问题的灯；英文标题下方有一行中文](https://wakenex.com/assets/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/fig3-1600.jpg?v=b822fcf006) *图片：WAKENEX* ## 什么会改变我们的判断 这里的判断是可证伪的，而接下来的几个月会检验它。如果那些具名的专家小组——指数时间假设上的 Impagliazzo、Paturi 与 Williams，以及杨–米尔斯上的 Gross 小组——在同行评审的场合公开确认，形式化的 Lean 命题忠实于那些经典猜想、而且证明是新颖且正确的，那么就是人类的审阅为这三条标题都背了书，而「Lean 检查本身就一锤定音」这一角色，会显得比这里所论证的更强。相反的情形也算数：如果审阅查出一处形式化缝隙、一个被悄悄削弱的命题、或是像 10 月 7 日那样的一次撤回，那么「验证只是一个狭窄的证人、而非一纸裁决」这个说法就会更站得住。无论哪种，盯住人，而不是那个对勾。那个对勾，已经把它知道的一切都告诉你了。 ## 来源与说明 - [OpenAI，《Building scientific understanding with academic communities》，关于三项由 AI 产出的结果（数学、计算机科学、物理）的公告，2026 年 10 月 26 日： （检索时直接访问返回服务器错误；内容与引述已与下列报道交叉核对）](https://openai.com/index/building-scientific-understanding-with-academic-communities/) - [unite.ai，《OpenAI Says Its Models Produced Three Proofs in Math, CS, and Physics》，2026 年 10 月 26 日—猜想名称、Lean 形式化日期、物理结果「由 David Gross 领衔的小组进行专家审阅」、具名研究者，以及 OpenAI 的「原始研究数据」与「牵头人／信息不对称」引述：](https://www.unite.ai/openai-says-its-models-produced-three-proofs-in-math-cs-and-physics/) - [datastudios.org，《OpenAI models: Exponential Time Hypothesis disproof, Kakeya, Yang-Mills proofs》，2026 年 10 月 26 日—时间线与 Lean 日期（CS 10 月 17 日、数学 10 月 19 日、杨–米尔斯 10 月 16 日）、运行时间界与 P 对 NP 未受触动、具名的验证小组、「一份 Lean 形式化……并不等于确认那条标题论断」、「三项论断没有一项经过同行评审」、内部／未公开的模型，以及 10 月 7 日因符号错误撤回三篇论文：](https://www.datastudios.org/post/openai-models-exponential-time-hypothesis-disproof-kakeya-yang-mills-proofs) - [FourWeekMBA，《OpenAI Says Its AI Refuted the Exponential Time Hypothesis》，2026 年 10 月 26 日—用通俗语言说明 Lean 检查是什么、不是什么，以及早期那场大体上持怀疑态度的公开讨论：](https://fourweekmba.com/ai-openai-says-its-ai-refuted-the-exponential-time-hypothesis/) - [Mikołaj Sienicki 与 Krzysztof Sienicki，《A Human Audit of OpenAI's AI-Generated Mathematical Proofs》，arXiv:2608.14673（2026，CC BY 4.0）—形式化验证确认一个证明遵守了它的形式规则，却不保证其成立性或新颖性；机器生成的证明需要在机械验证之外接受人工评估：](https://arxiv.org/abs/2608.14673) 关于 de Bruijn 准则与证明辅助器的背景：一个微小而可信的内核对照公理重新核对每一步推理，这认证的是形式化命题的可推导性，而不是形式化命题与非形式化猜想的吻合。 背景：杨–米尔斯存在性与质量间隙问题的官方表述，是由 Arthur Jaffe 与 Edward Witten 撰写的克雷数学研究所千禧年难题描述。 这是研究与分析，而不是关于数学是否正确的论断；截至撰写时，这些结果尚未经同行评审核实。 --- 引用格式：WAKENEX. "Verified Is Not Discovered: What a Proof-Checker Can't Tell You." wakenex.com, 2026-10-27. https://wakenex.com/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/ 网页版：https://wakenex.com/articles/verified-is-not-discovered-what-a-proof-checker-cant-tell/