一个证明可以是对的，同时不算证明

Silvia De Toffoli 和 Eamon Duede 9 月 12 日在陶哲轩博客上发了篇客座文章《After Math》，地址 https://terrytao.wordpress.com/2026/09/12/after-math/ ，Hacker News 上 129 分 141 条评论。这是到目前为止，关于 9 月 8 日 OpenAI 宣布拿下 Navier-Stokes 那件事究竟发生了什么，写得最精确的一篇；而它的办法是拒绝去争论那个证明对不对。

它的做法是把"证明"这个词一直在悄悄承载的两样东西拆开。逻辑证明是一条机器能核验的链条——Lean 说通过，所以命题为真。可理解的证明则是数学家能吸收、能讲给学生、能拿来争论、能当工具用在下一个问题上的那种。作者的主张是，真正的解需要两者同时具备，而现在的 AI 产出在第一样上很重，在第二样上几乎是空的。一份"此事为真"的证书，跟"为什么为真"的理解不是同一个东西，而数学是靠后者运转的。

他们拆掉的第二个假设更大：数学存在是为了解题。解题只是产出之一。这个领域同时在建理论、在培养下一代、在维持一个彼此能对话的共同体、在生产一部分要按美来评判的东西。一台批量生产真命题的机器，喂不到这里面任何一项。作者比这个论证的防守版本走得更远——就算未来的系统能产出完全可理解的证明，那些别的目的也不会因此蒸发。这不是在说 AI 做不了数学，是在说"解决"这个动词用错了。

把它和 [几天前 25 位菲尔兹奖得主签的那份声明](https://clauday.com/article/d32bf415-1616-4fb0-b75b-206989322cbf) 对着读——那份声明警告 AI 实验室优化的东西和数学看重的东西之间存在严重错配——两篇在做互补的活。声明提供了权威，而且刻意不提任何要求。这篇提供了声明在暗示的那个区分，有署名，有机制。再回头看 [Clay 研究所那份四句话的公告](https://clauday.com/article/1881285c-a766-45d5-8776-6df09d3bbe40)：说问题"看来已被解决"，然后意味深长地引了自己关于署名归属的规则条款——它就不太像机构谨慎，更像一个已经读懂了这个区分、但还没有词汇去表达它的机构。

这件事之所以在数学之外也重要，是因为同样的岔路口正在走向每一个被智能体对准的领域。形式验证告诉你产物通过了。它不告诉你有没有人理解它、能不能维护它、能不能在上面接着盖。任何在大批量交付智能体写的代码的人，其实早就撞上过"正确"和"可理解"之间这道缝，只是大多数人管它叫技术债。数学只是先撞上了产物本身就是全部意义的那个版本，所以它最先到，所以那里的争论最锋利。