菲尔兹奖天才发现：自己证明有错

数学，是人类文明中最不容置疑的学科。

物理有范式革命，生物有可重复性危机，经济学预测年年打脸，但数学不一样。

数学有证明。

一个定理一旦被证明，就是永恒的、绝对的、不可推翻的。

真的吗？

2013 年秋天，普林斯顿高等研究院（IAS）的一场晚宴上，一位 51 岁的俄裔数学家倒扣了自己的酒杯。

他刚确认了一件事：自己那篇让学术界奉为经典的早期论文，主定理根本就是错的。

所谓 "有个小缺口可以修补" 并不成立；这个错误彻底、结构性且不可挽救，早在 15 年前就有人指出了这个问题。

但因为这位天才的名字太响亮，几乎没有人认真对待那个反对声音。

他的名字叫弗拉基米尔?沃耶沃茨基（Vladimir Voevodsky），2002 年菲尔兹奖得主，那是数学界的 "诺贝尔奖"。

▲ X 用户 Nora（@0xNoraa）的长视频帖讲述了这段数学史

天才少年与一篇 "改变一切" 的论文

故事要从 1980 年代末的莫斯科说起。

沃耶沃茨基是一个极不标准的天才。

他厌恶学院体制，疏于上课，被莫斯科大学 "退学" 处理，连本科文凭都没拿完整。

但这不妨碍他在数学世界里横冲直撞，他从导师 George Shabat 手中拿到了格罗滕迪克（Alexander Grothendieck）的法文手稿 Esquisse d'un Programme，为了读懂它自学了法语。

那一年，他才是个大一新生。1988 年或 1989 年，他遇到了志同道合的 Michael Kapranov。

两人一拍即合，合写了一篇关于∞?群胚（∞?groupoids）的论文，宣称给出了格罗滕迪克关于高维代数结构与同伦论联系的严格表述与证明。

这篇论文成了他学术起飞的第一级火箭。

正如数学博客作者 Orr Shalit 后来所写：这是推动他 "明星生涯" 的起点论文。

▲ 圣安德鲁斯大学 MacTutor 数学家传记：1966 年生于莫斯科，2017 年卒于普林斯顿

此后的轨迹像开了挂：1990 年夏天，Kapranov 绕过常规申请流程把他安排进了哈佛读研。

他随后专注于代数几何中的动机上同调（motivic cohomology），一个当时被认为 "高度推测、基础不牢" 的领域。

2002 年，凭借在这一方向上的突破性工作，他拿到了菲尔兹奖。

36 岁，站在数学世界的最高峰。

那个被无视了 15 年的反例

但暗流早已涌动。

1998 年 10 月，法国数学家卡洛斯?辛普森（Carlos Simpson）在 arXiv 上传了一篇论文，标题平淡：Homotopy types of strict 3?groupoids。

文中给出的结论却十分尖锐：在相当一般的条件下，严格 n?群胚不可能实现二维球面的 n?型。

这与 Kapranov 和沃耶沃茨基那篇经典论文的主定理直接冲突。

▲ Carlos Simpson 的论文摘要页：提交于 1998 年 10 月 9 日，编号 math/9810059

那么，数学界炸锅了吗？

并没有。

原因很荒诞，却非常真实：Simpson 能证明 "主定理不可能为真"，却无法指出原文具体哪一步出错。

沃耶沃茨基和 Kapranov 考虑过这个批评，互相说服 "不适用"，然后继续前行。

这就陷入了一个极其诡异的僵局：一边有反例说 "不可能"，另一边有论文说 "我证了"。

谁错了？

没人能给出决定性判断。

而接下来发生的事，才是整个故事中最令人不寒而栗的部分。

数学社区用沉默回应了这场冲突。

沃耶沃茨基的结果停止被后续工作引用，也几乎无人正面挑战他。

Simpson 的反例论文就像一块石头沉入水底，涟漪散尽，水面恢复平静。

沃耶沃茨基后来在 2014 年 IAS 演讲中，用 "Outrageous"（令人发指）来形容这种局面，并总结了两个致命因素：

第一，反例方找不到原文漏洞，所以无法 "定罪"；

第二，基于声誉的互信系统，到 Simpson 发文时，Kapranov 和沃耶沃茨基已经是学术明星。

谁会去正面质疑菲尔兹奖级别的人物呢？

▲ 2014 年 3 月 26 日，他在 IAS 发表演讲《Univalent Foundations》，用第一人称讲述了这段 "噩梦"

直到 2013 年秋天，距 Simpson 论文整整 15 年，沃耶沃茨基才终于完全接受：自己错了。

Nautilus 杂志引用他自己的原话："plainly wrong"。

这里没有可供修补的缝隙，主定理根本就是错的。

"我一生中最大的失败"

类似的 "信任黑洞"，他还遭遇过一次。

更早之前，在 1999/2000 年的 IAS 讲座系列中，当菲尔兹奖得主皮埃尔?德利涅（Pierre Deligne）坐在台下一步步做笔记核查时，沃耶沃茨基发现：自己关于动机上同调的另一篇重要论文中，一个关键引理也是错的，且原表述无法挽救。

好消息是，这个方向上他最终找到了一个较弱但足够用的替代引理，核心结果得以保存，更正版 2006 年发表。

坏消息是，自 1993 年起，多个研讨班研读过这篇论文并依赖它，却没有任何人发现错误。

他在演讲幻灯里打了感叹号："一位受信任作者写出的、难以核对又看起来像已知正确论证的技术段落，几乎从不会被详细检查。"

▲ "最可怕的是，指出错误的人因对方声望更高而被忽视了多年，声誉成为验证的替代品"

这就是两条裂缝的区别：动机论文的引理错误是工程式修复，相当于大厦里换了根梁柱，楼还在；而∞?群胚方向的主定理为假，是整栋楼坍塌，研究纲领层面的破产。

如果只说 "一位天才发现自己证明有错"，这两种截然不同的失败便被彻底抹平了。

他用余生建造的 "机器裁判"

这些经历在他心中触发了一次存在主义级别的危机。

他开始思考一个可怕的问题：如果连比较简单的论证都要数年才能被揭错，那更复杂的工作呢？

谁来保证自己，或者任何人，没有遗漏？

答案指向一条当时几乎被主流数学界视为异端的道路：让计算机参与验证数学推理。

所谓证明助手（proof assistant），就是一类软件，要求人把定义、定理与推理步骤写成机器可检查的形式语言，软件按逻辑规则逐步核对每一步是否合法。

它不会 "发明" 深刻思想，但能大幅降低 "看起来对、其实有洞" 的风险。

▲ Nautilus 杂志标题：《在数学中，错误已不再是过去的样子》，2015 年对沃耶沃茨基的深度访谈

但在 2000 年前后，他寻找实用工具时几乎找不到。

文化障碍同样明显：跟数学家提 "计算机验证"，对方要么搬出哥德尔不完备定理说 "这不可能"（他认为这完全跑题），要么觉得形式化会把创造性工作变成 "编码苦役"。

他在演讲中感叹：坚持推进这条路的人少得可怜。

他的解决方案远不止 "用现有软件" 这么简单，他认为既有数学基础本身就不适合作为日常可计算的工作语言。

于是他转向了同伦类型论（Homotopy Type Theory, HoTT）与单值基础（Univalent Foundations）：把类型论中的 "相等" 概念与同伦论的连续变形联系在一起，打造一套天然便于计算机验证的新数学语言。

他把后半段人生都投入了这项工作。

▲ Homotopy Type Theory 官方站点：连接 Martin?L?f 依赖类型论与抽象同伦论的新基础

他没能看到的未来

2017 年 9 月 30 日，沃耶沃茨基在普林斯顿突然去世，年仅 51 岁。

他没能看到接下来发生的事：2020 年代，Lean 语言与 Mathlib 数学库爆发式增长，菲尔兹奖得主陶哲轩公开学习 Lean 并用它形式化多项式 Freiman?Ruzsa 猜想的证明；Peter Scholze 的凝聚数学核心结论在 Lean 中被机器验证通过。"蓝图（Blueprint）+ 依赖图 + 全球协作填 sorry" 成了新一代数学生产模式。

▲ 陶哲轩 2023 年博文：用 Lean4 + Blueprint 协作形式化 PFR 猜想证明，"内核检查，而非人际信任"

更激进的实验也在涌现。

数学家 Bartosz Naskr?cki 展示了用 AI 工具将论文自动形式化为约 5000 行 Lean 代码，编译通过即构成正确性证书，甚至修正了原文中的不一致与缺口。

审稿人的角色正在收缩为 "核对定义与定理语句是否说对了人话"。

▲ "在某些数学领域，我们距离证明有效性记录方式的巨大转变已经不远了"

今天工作数学家用的主流工具是 Lean，而非沃耶沃茨基倡导的 HoTT/Coq 路线，CNRS 研究者 Dominique Larchey?Wendling 在讨论中专门做了这个区分。

但这并不削弱他的核心遗产：问题比任何单一系统更持久。

是他以菲尔兹奖得主的身份，把 "基础必须可计算地用于日常推理" 这个被嘲笑了几十年的主张，重新推回了数学界的议程中心。

他留下的警告

在他 2014 年那场用第一人称讲述的 IAS 演讲中，有一段话击中了所有人：

数学家的工作，5% 是创造性洞见，95% 是自我核验。

证明助手迫使作者放弃 "类似可证"" 显然 " 等捷径。

而他更深层的警告是：如果人人为了抢先发表而省略细节，学生会把省略学成规范，标准会从内部溶解。

这不仅仅是数学的问题。

把 "专家声望" 当作 "已核实" 的替代品，把 "没有人反对" 当作 "正确" 的证据，把 "太复杂所以不检查" 当作可接受的理由，这是每一个以专业权威降低核对成本的知识行业都在面对的系统性风险。

沃耶沃茨基留下的话，值得所有人反复咀嚼：

"很多我们称为 ' 已证明 ' 的东西，其实只是 ' 被信任 '。"