AREX Viewpoint Article
Why Mathematicians Stopped Trusting Their Own Proofs — Kevin Hartnett
导读
2026 年 9 月，Epoch AI 公布新基准 FrontierMath Erdős：它从数学家 Paul Erdős 留下的问题里选取 68 道截至 2026 年 8 月仍然开放的难题，由 Thomas Bloom 挑选并以 Lean 形式化，要求 AI 系统在固定预算内逐题给出证明或否证。按配套论文的记录，每题预算约 300 美元，而早期系统在这批题上的得分仅约 3%。
这条消息的分量，在于它把“AI 做数学”的靶子从有标准答案的竞赛题，换成了数学界自己尚未解决的问题，并让 Lean 承担最终裁判。Epoch AI 说明，这些题目在 2026 年 8 月基准成型时均处于开放状态。个位数的得分说明，把模型的推理落到可被机器检查的证明上，仍是前沿而非既成事实——这也正是理解这支影片的入口。
Machine Learning Street Talk 于 10 月 26 日发布的纪录片《Mathematics Just Changed Forever》，恰好在基准铺开、结果仍在累积的当口讨论同一件事。影片在 58:43 处处理“2026 年的 AI 数学与陶哲轩的实验”，参考列表也直接列出 FrontierMath Erdős。它转述称，在 Epoch AI 的固定预算测试中，一个预发布的 OpenAI 模型证明了 Erdős 问题 126、又以反例否证了问题 74，两项结果都经 Lean 验证。这类说法究竟意味着什么，需要影片提供的概念工具来判断。
影片最关键的补充是“形式化差距”。检查器认证的是从形式化陈述到结论的推导链条，却不认证这个陈述是否忠实于人类真正想问的猜想。因此，“某题已在 Lean 中通过验证”并不等于“该定理为真”，信任被转移到了更上游——目标陈述的选择上。放到 FrontierMath Erdős 上，一道题被机器判为“已证明”，首先得追问：被证明的是形式化者写下的那条陈述，还是 Erdős 原本的问题？
影片进一步指出，Lean 能验证证明，却无法验证定义，因为定义在逻辑上没有真假，只有是否恰当。基准的可信度因此取决于人的判断：谁来形式化、按什么约定理解“图”“和”“存在”。影片中舒尔策的担忧正落在这里——若 Lean 中的定义本身有偏差，机器仍可能“正确”地验证一个并不成立的结论。成绩好坏不只在模型能力，也在形式化者把数学意图翻译成代码时的准确性。
影片也交代了这套基础设施为何值得托付。1998 年黑尔斯完成开普勒猜想证明后，《数学年刊》的审稿人面对深埋在代码中的庞大体量无从判断；舒尔策的液态张量证明同样几乎无人逐行读过，最终是 Lean 社区第一批把它逐行梳理并确认其正确。正是这类“没有人真正读过”的危机，把 Lean 从微软研究院的副项目推成数学界用来自查的工具。理解了这段历史，才能理解 FrontierMath Erdős 为何选择 Lean 而非自然语言作裁判。
所以，这支影片此刻的价值，不是宣布“机器已经会做数学”，而是交给读者一套阅读 AI 数学头条的判断标准：区分“正确”与“有用”，分清“推导被检查”与“目标被确认”，并在看到“Lean 验证通过”时追问它证明的是不是我们真正想问的东西。当 68 道开放 Erdős 问题被摆上机器可检查的靶场，真正稀缺的能力或许已不是证明本身，而是提出恰当的定义、选择值得证明的命题。
核心结论
- 数学信任的基础正在从专家人工审阅转向可独立核验的形式化证书：黑尔斯和舒尔策的案例共同证明，当证明体量超出人类可读范围时，传统审稿机制已经失效。Lean 社区逐行检查液态张量证明并确认其正确，标志着机器核验成为新的信任锚点。
- Lean 的可信性来自极小的可信内核，而非整个系统的无缺陷：内核把假命题验证为真是不可饶恕的罪，因为这会打开验证无数错误命题的大门。独立检查与内核最小化是对历史上内核缺陷的直接回应，也是理解形式化验证为何可靠的技术基石。
- 形式化工具要获得数学家接受，必须从验证正确性转向促进发现与理解：数学家抵制形式化的根本原因在于，验证已知正确的结果远不如发现新数学有吸引力，而德布鲁因因子的高昂成本加剧了这种抵制。Mathlib 的软件工程式重构表明，形式化本身可以带来对数学结构的新理解，这才是它真正的价值所在。
- AI 与 Lean 的结合正在改变数学发现，但正确性不等于有意义：AlphaProof 在 IMO 达到银牌水平，2026 年 AI 已能解决开放研究问题并经 Lean 验证，但数学家担心 AI 的搜索缺乏对正确抽象的审美，可能走向与人类数学分叉的路径。形式化差距的存在意味着机器验证的可能是错误的东西，数学仍然是人类活动。
- 自动形式化加速了数学数字化，却制造了理解债务和规格说明瓶颈：LLM 能快速将论文翻译为 Lean 代码，但生成的代码缺乏对正确抽象的追求，导致代码库难以维护。这一困境从数学延伸到软件工程：当 AI 可以自主生成代码，瓶颈从写代码转向了写规格说明和审查。
观点拆解
1. 计算机证明从“无法被审阅”到“机器终于读过了”的转变，正在重塑数学的信任基础
-
黑尔斯的开普勒猜想证明暴露了传统数学审稿机制的极限：黑尔斯在1998年完成证明后，将成果提交给《数学年刊》，但审稿人面对的是深埋在计算机代码中的庞大计算体系，无法判断整体是否成立。这揭示了传统依赖少数专家人工审阅的信任机制，在证明体量超出人类可读范围时已经失效。
“他把证明丢给了《数学年刊》的编辑们——这是该领域最负盛名的期刊——而他们基本上不知道该如何审阅它，不知道如何把它送给其他数学家去验证其正确性。”
“审稿人看过的每一部分似乎都是正确的，但整个证明是一座深埋在计算机代码中的庞大计算大厦，很难确定它们如何衔接在一起，以及最终是否真的得出了黑尔斯所声称的证明。”
-
舒尔策的液态张量证明同样面临“无人真正读过”的信任危机：菲尔兹奖得主彼得·舒尔策发现，他的合作论文中六页技术计算部分，连普林斯顿和哈佛的同行都只是粗略浏览，没有人真正逐行读过。这进一步说明，即便是顶尖数学家的关键工作，在传统审稿流程下也可能处于未被真正验证的状态。
“我们没读细节。他说，每个人都这么说。他问过普林斯顿的人，也问过哈佛的人。每个人都这么说。他逐渐确信，没有人真正读过他的工作。”
“他说，归根结底，这些材料看起来技术性很强，但很多内容其实是本科水平的东西。所以也许你们的系统可以检查这些材料。”
-
Lean 社区逐行检查液态张量证明，机器核验成为新的信任锚点：Lean 社区成为第一批真正逐行阅读舒尔策证明的人，他们用形式化工具检查了关键部分，并找到了一个简化论证。最终机器确认证明正确，舒尔策因此感到兴奋——因为终于有东西真正“读过”了他的工作。这标志着数学信任机制从人工审阅转向算法可独立核验的形式化证书。
“我们必须开始阅读这些材料，必须真正去读它。我们很可能是第一批真正阅读它的人，第一批没有粗略浏览的人。我们开始用细齿梳子逐行梳理，结果找到了一个简化。”
“六个月后，我们检查了彼得担心的那个关键问题。彼得说，不，我认为它是对的。我的合著者达斯汀·克劳森也认为它是对的。没有其他人读过它。也许它是错的。六个月后，我们替他读完了。他说，没问题，它是对的。机器说它是对的。”
“这些系统确实有用，因为它们让我学到了证明是如何运作的。我们找到了其中一部分更概念化的论证，而且终于有东西真正读过它了。”
2. Lean 的可信性不依赖整个系统，而依赖一个极小的“可信内核”
-
信任被刻意压缩到一个极小的内核，而不是分散在整个 Lean 系统上：Lean 本身规模庞大、必然存在大量缺陷，但用户并不需要信任整个系统。设计者把信任边界收缩到一个尽可能小的内核上，只有内核的验证结果才构成最终判断。这意味着系统的可信性来自“最小化必须信任的部分”，而非追求整个软件没有错误。
“我们有一个“小型可信内核”的概念。Lean 很庞大，有数不清的缺陷。但要在 Lean 中信任我们的结果，我们只信任内核。那要小得多。”
-
内核把假命题验证为真，是比拒绝真命题严重得多的“不可饶恕之罪”：内核可能犯两类错误：把真命题判为假，或把假命题判为真。前者只是制造障碍和不便，后者却会打开验证无数错误命题的大门，因为后续错误都可以由最初的假命题“合法地”推导出来。这种不对称性决定了内核设计的首要目标是杜绝假命题被验证为真。
“内核的“不可饶恕之罪”是把假命题验证为真，这远比把真命题拒绝为假更糟糕。把真命题判为假只是制造障碍，是一种不便。但把假命题判为真，就打开了验证无数更多假命题的大门，而所有这些假命题都由最初那个假命题来辩护。”
-
独立检查与内核最小化，是对历史上内核缺陷的直接回应：Agda、Coq 和 Isabelle 等系统都曾在内核中出现过允许验证假命题的缺陷。面对这一历史教训，de Moura 的答案是让用户能够构建自己的内核进行独立检查，而要使这一方案可行，内核必须保持尽可能小、代码行数尽可能少。HOL Light 的极小内核因此成为他欣赏的范本。
“多年来，Agda、Coq 和 Isabelle 等交互式定理证明器的内核中都曾包含允许用户验证假命题的缺陷。他的答案是独立检查：让用户构建自己的内核。”
“为了使这一选择切实可行，de Moura 知道他需要把内核保持得尽可能小、尽可能极简，用尽可能少的代码行数来实现。在已有的交互式定理证明器中，de Moura 欣赏 HOL Light 的极简性，它有一个非常小的内核。”
3. 数学家对形式化的抵制源于“正确性”不是他们最关心的价值
-
数学家抵制形式化，是因为“验证正确”远不如“发现新数学”有吸引力：黑尔斯投入二十人年形式化开普勒猜想，最终只得到“证明正确”的保证，而没有产生新数学。对数学家来说，这种回报远不如新发现令人兴奋，尤其是在他们本来就已经相当确信结果正确的情况下。这说明形式化工具若只定位为“正确性检查器”，很难打动主流数学家。
“黑尔斯投入二十人年形式化他的开普勒猜想结果，最后得到的只是确认这件事是正确的。这远不如获得新数学和新发现那么令人兴奋。”
“在大多数情况下，数学家知道事情是否正确。他们并不被正确性问题困扰。”
-
德布鲁因因子高达二十比一，使形式化的时间成本难以被数学家接受：形式化需要为每一行非形式数学写出二十行甚至更多的 Lean 代码，这种极高的转换成本让数学家看不到投入时间的理由。既然他们最关心的是发现新数学，而形式化目前主要只服务于验证正确性，抵制就成了一种理性反应。
“有一个叫德布鲁因因子的概念，它指的是你在 Lean 中为每一行非形式数学——比如 LaTeX PDF 中的一行——需要写的代码行数，这个数字非常高，通常是二十比一，往往更高。”
“数学家通常看不到投入额外时间仅仅为了验证某件事的正确性有什么理由。这就是抵制的真正来源。他们看不到 Lean 对他们最关心的事情——发现新数学——有什么用处。”
-
仅以“检查正确性”为由推广形式化，无法吸引数学家：形式化之后，数学家并没有因此知道更多数学内容，也没有改变“谁知道它”的局面。因此，单纯用正确性论证来推广形式化，并没有引起多少数学家的兴趣。形式化要获得主流接受，必须证明自己有助于理解和发现，而不仅仅是验证。
“我想在形式化之后，你到底多知道了什么？而且是谁知道了它？仅仅从检查正确性的角度来论证形式化，并没有让多少数学家感兴趣。”
4. Mathlib 的本质不是“把数学翻译成代码”，而是对数学进行软件工程式的重构
-
形式化让数学项目变成可以拆分、协作且无需逐行人工检查的软件工程项目：Kevin Buzzard 指出，大型数学项目本质上可以被视为工程项目：项目架构师把大问题拆成小块，让包括高中生在内的协作者填充细节，而 Lean 保证了每一块证明的正确性，因此架构师不必再手动检查证明是否成立。这改变了数学协作的信任机制，使大规模合作成为可能。
“大型数学项目可以被视为工程项目。Johan Commelin 是一位非常硬核的数学家，但他也是一位软件工程师。他把大项目拆成小块，人们可以填充这些小块。他就像项目的架构师，人们开始填补空缺，而他不需要手动检查。”
“你不必一直思考证明是否正确。他知道证明是正确的。他可以清理、改进，但证明是正确的。这很有价值。”
-
Mathlib 只收录“成熟、打磨过、处于正确一般性”的数学，而不是边界上仍然混乱的想法：Kevin Buzzard 强调，数学在边界处往往尚未完全成形，而 Mathlib 想要的是已经被充分理解、处于正确抽象层次的“抛光过的数学”。把混乱的概念过早放入库中，后续一旦被推广或简化，就可能导致整个体系需要返工，因此社区宁愿第一次就做对。
“我们想要放进库里的，是那些真正被充分理解、并且存在于正确一般性层面的想法。我们想要的是经过打磨的数学。那些仍然有些混乱的东西，我们可以尝试教给软件，但我们不一定想把它加入库中。”
“你不想把某个概念放进库里，然后它被推广和简化了一点，接着你就需要重做整个东西。我们尽量避免这种情况。我们喜欢第一次就做对。”
-
形式化迫使数学家像软件工程师一样思考模块、接口和 API，并由此获得对数学结构的新理解：Jeremy Avigad 观察到，当数学家必须把自以为理解的数学形式化时，他们不得不高效地表示概念、封装信息、暴露接口，思考模块之间如何交互。这种软件工程式的思维方式不仅服务于验证，更让数学家以新的方式重新理解数学本身的结构。
“当你回到一段你以为自己已经理解的数学，但现在你必须把它形式化，你必须以计算机能够理解和检查每一个细节的方式来表示它，你会发现自己变得非常高效，尤其是在如何表示概念并把它们组合起来方面。”
“你开始用计算机科学家所说的 API 来思考它们。你封装一些东西，暴露一些东西，哪些信息对其他人公开，哪些是内部实现。数学家发现，用这种软件工程的方式思考数学很有用：不同的模块是什么？各个部分是什么？它们如何交互？接口是什么？”
“这实际上是在探索数学的结构，以及各个部分是如何组合在一起的。我们在这些非常精确的规则之上建立了非常复杂的大厦，理解如何从底层的简单规则达到那种复杂程度，真的很了不起。”
5. AI 与 Lean 的结合正在改变数学发现的形态，但“正确”不等于“有意义”
-
AlphaProof 用 Lean 验证证明，在 2024 年国际数学奥林匹克达到银牌水平：DeepMind 设计的 AlphaProof 基于 AlphaGo 的架构，通过强化学习从中学水平逐步爬升到竞赛水平，最终在 2024 年 IMO 上取得银牌分数。关键在于，它解题的方式是输出 Lean 证明，再由 Lean 验证其正确性，这使“机器做数学”第一次与形式化验证深度绑定。
“最终，它取得了银牌水平的分数，而它解题的方式是输出 Lean 证明，然后用 Lean 来验证它们。”
“数学是一个非常有效的 AI 训练环境，因为你在最后会得到一个清晰的奖励信号：它有没有把问题做对？”
-
到 2026 年，AI 已在固定预算下解决开放研究问题，且结果经过 Lean 验证：AI 数学能力从竞赛题延伸到了开放研究问题。在 Epoch AI 的固定预算测试中，一个预发布的 OpenAI 模型证明了 Erdős 问题 126，并通过找到反例否证了问题 74，两项结果都在 Lean 中得到了验证。这表明形式化验证正在成为 AI 数学成果可信度的基础设施。
“到 2026 年 9 月，AI 系统已经在处理开放研究问题。在 Epoch AI 的固定预算测试中，一个预发布的 OpenAI 模型证明了 Erdős 问题 126，并通过找到反例否证了问题 74。两项结果都在 Lean 中得到了验证。”
-
AI 的搜索缺乏人类对“正确抽象”的审美，可能无法复现人类数学路径：数学家们担心，如果让 AI 从基本公理出发重建数学，它的搜索只受“严格正确”驱动，而不受人类对概念完整性、扩展性和美感的判断引导。几位数学家的共识是，这样的系统可能连有理数之后的人类数学路径都无法复现，而是会走向与人类数学分叉的方向。
“我交谈的三位数学家的共识是，它不一定会发现比有理数更多的东西。如果你沿着人类对数学的理解从有理数开始推进，几乎在最最开始的地方，他们预计计算机数学就会与人类发现的数学分道扬镳。”
“我认为原因是，我们对正确的抽象有一种感觉。这些令人满意的概念和定义让我们觉得对、觉得完整、觉得有扩展力。而计算机在做这种只追求严格正确的搜索时，它的搜索不会被同样的价值观所引导。”
6. 形式化验证的真正瓶颈不在证明推导，而在“形式化差距”——机器证明的可能是错误的东西
-
机器验证只能保证推导正确，不能保证“证明了正确的东西”：检查器认证的是从形式化陈述到结论的推导链条，而不是形式化陈述本身是否忠实于人类真正想表达的猜想。这意味着“已通过验证”并不等于“该定理为真”，信任只是从证明过程转移到了目标陈述的选择上。
“一个经过检查的证明，仍然可能是对错误对象的证明。”
“检查器认证的是推导过程，但它不认证人类对目标的选择。这就是形式化差距。信任基本上被转移到了上游。”
-
定义本身没有对错，只有是否恰当——而恰当性无法被机器判定：在数学中，提出正确的定义往往是核心工作，但定义在逻辑上并不存在“真”或“假”的属性。Lean 可以验证证明，却无法验证定义是否忠实于数学家约定俗成的理解，这构成了形式化方法的一个根本局限。
“你怎么知道用 Lean 写下的定义，忠实于数学家们约定俗成地理解的那个对象的定义？”
“Lean 可以验证证明，但它无法检查定义，因为从逻辑上讲，定义没有对错。它们只是你所说的那样。”
-
舒尔策的结论：数学仍然是人类活动，因为真正的确认需要人在头脑中拆解整个证明：舒尔策的担忧揭示了形式化验证的深层悖论：要真正确认机器做了正确的事，人仍然需要在自己的头脑中重新拆解和审视整个证明。这意味着形式化工具可以辅助数学，但无法取代数学家对定义恰当性和证明意义的判断。
“舒尔策担心，如果 Lean 中的定义是错的，没有人能看出来。Lean 可能会验证一个证明是正确的，即使它实际上并不正确。”
“我目前的感觉是，数学仍然是一项人类活动。因为如果我要真正检查计算机做了正确的事，我就必须在头脑中拆解整个证明，并检查它是否真的成立。”
7. 自动形式化是一把双刃剑：它加速了数学数字化，但也制造了“意大利面怪兽”式的理解债务
-
自动形式化大幅降低了数学数字化的门槛，并有望加速 Mathlib 的增长：Lean 的繁琐语法一直是数学家进入形式化领域的障碍，而 AI 工具让研究者可以像写普通代码一样生成 Lean 代码，不必先掌握全部语法。更关键的是，自动形式化已经能够把整篇数学论文或教科书快速转换为 Lean 代码，速度远超人类团队，这为 Mathlib 的快速扩充带来了切实希望。
“显然，有了智能体编程，你不需要学会所有 Lean 语法，可以像写 JavaScript 那样来写代码。”
“有一个梦想是，你可以拿一本完整的数学教科书，展示给 AI，让它自动翻译、转换成 Lean 代码。这就是自动形式化的过程。”
“你现在可以把一篇数学论文交给大语言模型，它能在人类团队完成同样工作所需时间的一小部分内，输出对应的 Lean 代码版本。”
-
AI 生成的代码缺乏对“正确抽象”的追求，正在制造难以理解和维护的代码库：AI 在自动形式化时往往只是盲目翻译，不关心代码是否处于恰当的抽象层级，也不追求让结构变得清晰易用。结果是代码虽然通过了检查，却变得冗长、复杂、难以驾驭，人类数学家会感到本应顺畅推进的工作被无谓地拖慢。
“AI 工具只是看到书里的内容，完全不思考，就盲目地把人类写的数学翻译成 Lean 代码，并不真正关心是否让事情变得简单。”
“如果不得不在本应具备的普遍性层级之外艰难地硬啃这些内容，事情会变得复杂得多。作为人类，当你感觉自己本应轻松越过这些内容时，你不会想费力地硬闯过去。”
“我们现在遇到了一个真正严重的问题：意大利面怪兽。我们正在写我们不再理解的代码。我们不再理解自己的代码库了。”
-
核心问题从“如何验证”转向“如何在不理解的情况下管理复杂性”：自动形式化让代码可以快速生成并通过检查，但通过检查的证明仍然可能是对错误目标的证明。信任从推导过程本身转移到了上游：人类必须确认形式化陈述真正捕捉了原始数学意图。这意味着数学社区面临的挑战不再只是验证正确性，而是在代码库快速膨胀且难以理解的情况下，建立可检查的规范来管理复杂性。
“我们需要有某种方式来构建计算机可检查的规范。但一个被检查过的证明，仍然可能是对错误命题的证明。”
“检查器认证的是推导过程，但它并不认证人类对目标的选择。这就是形式化鸿沟。信任基本上已经向上游转移了。”
8. 形式验证正在从数学走向 AI 软件生命周期，但规格说明本身成为新的瓶颈
-
AI 已能将真实 C 代码翻译为 Lean 并证明关键往返性质：Kim Morrison 使用 Claude 智能体把 zlib 的 C 代码翻译成 Lean 实现，并证明了“任意压缩级别、任意数据，压缩后再解压都能还原原始数据”这一核心性质。这说明 AI 辅助形式验证不再只是数学玩具，而是开始触及真实软件。
“AI 成功把代码从 C 翻译到 Lean，然后不断修复 Lean 实现，直到它通过 C 版本自带的测试套件。接着它证明了：对任意压缩级别、任意数据，如果你先压缩再解压，就能拿回原始数据。”
-
规格说明不完整时，验证通过也不等于得到用户真正想要的东西：专家指出，如果人类仍在循环中审查代码，问题还不算严重；但一旦放任 AI 自主生成代码而不再查看，就必须确保规格说明覆盖所有方面。否则实现可以满足所有已写出的性质，却仍然不是用户真正想要的。
“一旦你让 AI 放开手脚，而你甚至不想再看代码，那么覆盖所有方面就变得极其重要。否则，你可能得到一个满足你所有性质的实现，但你并没有完整说明你真正想要什么。你并没有真正得到你想要的东西。”
“正是出于这个原因，有人怀疑形式验证是否会被广泛用于验证所有这些 AI 生成代码的正确性。对于在那个层级上运行的程序，根本没有办法写出规格说明。”
-
AI 软件生命周期的瓶颈正从写代码转向写规格说明与审查：智能体编码的效用目前完全卡在审查和验证阶段，但 AI 本身可以反过来帮助撰写规格说明，不必全部手工完成。因此，形式验证有望在新的 AI 驱动软件开发流程中扮演越来越重要的角色。
“智能体编码的效用目前完全被审查和验证阶段卡住。我认为 AI 本身让软件验证变得强大得多，因为你可以用 AI 来撰写这些规格说明本身。它们不必手工编写。基本上，我认为软件程序的形式验证将在新的 AI 驱动的软件开发生命周期中扮演越来越重要的角色。”
总结
形式化验证正在改变数学和软件的可信基础，但它带来的最大启示不是“机器可以证明一切”，而是“正确性从来不是终点”。当证明可以被机器逐行检查，当 AI 可以生成通过验证的代码，真正稀缺的能力变成了提出正确的定义、选择恰当的抽象、判断什么值得证明。数学仍然是人类活动，因为理解、审美和意义判断无法被内核验证，也无法被搜索算法替代。
信息源
视频来源
- Mathematics Just Changed Forever — Kevin Hartnett：
外部资料
- Announcing FrontierMath Erdős：
- AI in math: Data & research：
- FrontierMath Erdős：
- Thomas Bloom on X：