逻辑与有效推理

第一部分

三段论的形式结构

正文在向你展示了「所有人都是凡人」之后便匆匆掠过。但亚里士多德的词项逻辑有着值得一读的内部架构，以及一条耗时两千年才被察觉的裂痕。

每一个经典的直言命题都有四种形态，中世纪的逻辑学家用两个拉丁词——意为「肯定」的 affirmo 与意为「否定」的 nego——中的元音字母为它们命名。A：全称肯定（所有 S 都是 P）。E：全称否定（所有 S 都不是 P）。I：特称肯定（有的 S 是 P）。O：特称否定（有的 S 不是 P）。将这四个命题置于正方形的四个角，你就得到了西方思想史中最古老的图表之一：对当方阵 (square of opposition)。它描绘了四种命题之间如何相互支持或反驳：A 和 O、E 和 I 互为矛盾关系，即二者必定一真一假；A 和 E 是反对关系，它们不能同真，但可以同假。这是一个关于「量」的精巧推理机器，数世纪以来，它曾被灌输进每一位受过教育的欧洲人的脑海。

现在来看看那条裂痕。注意垂直的边缘，这被称为差等关系 (subalternation)：经典的对当方阵认为，如果「所有 S 都是 P」为真，那么「有的 S 是 P」也必然为真。从全称下降到特称。这听起来理所当然——如果所有的乌鸦都是黑的，那么显然「有的乌鸦是黑的」。但它暗中带入了一个亚里士多德从未明示的假设：即世界上至少存在一个 S。看看它是如何失效的：「所有非法入内者都将被起诉」这句话，即便在没有非法入内者出现的太平盛世，地主说出来也依然是真的。但差等关系会强行推导出「有的非法入内者将被起诉」——而这断言了非法入内者的存在。更糟的是：「所有独角兽都是白色的」听起来人畜无害，但经典的对当方阵却能从中推导出「有的独角兽是白色的」，通过纯粹的逻辑召唤出了一只独角兽。这就是所谓的存在蕴涵问题 (problem of existential import)，这正是弗雷格的量词（我们在正文中见过）被发明出来要弥合的精确缝隙。

现代谓词逻辑将「所有 S 都是 P」解读为一个谨慎的条件句——「对于任何事物，如果它是 S，那么它就是 P」。当世界上根本没有 S 可供检查时，这个命题就自动为真（这被称为「空真」命题，就像你因为从未做出过相关举动而轻易守住的诺言）。全称不再蕴涵特称。这就是为什么「所有独角兽都是白色的」和「所有独角兽都是蓝色的」可以同时为真：因为独角兽的数量为零，凡是形如「所有独角兽都……」的全称条件句都会空真；但「有些独角兽是白色的」这类特称命题并不会因此成立。弗雷格方案的代价是放弃了方阵中一些整齐的推理，但这是一个值得的交易，也是一个绝佳的案例，展示了对直觉的形式化如何揭示出那些无人察觉的隐藏假设。

形式证明如何构造

正文谈到了「有效形式」，但从未展示逻辑学家是如何步步为营地「构建」证明的。证明有两种伟大的流派，它们之间的博弈塑造了二十世纪的逻辑。自然演绎 (natural deduction)由格哈德·根岑于 1930 年代发明（斯坦尼斯瓦夫·亚希科夫斯基也独立提出了这一概念），它试图模仿人类真实的思考方式：你先作出临时假设，推出后果，再「解除」这个假设——这正是「假设其反面……」这一证明步骤的精髓。与之配套的相继式演算 (sequent calculus)同样出自根岑之手，它更具对称性，对机器也更友好，它将推导过程看作一套明确记录前提与结论的形式系统。

随后，根岑证明了他的系统的一个深刻特性：切消去定理 (cut-elimination theorem)（他的「Hauptsatz」，即核心定理）。通俗地说，它意味着任何通过巧妙的中间引理绕路的证明，原则上都可以重写为一个永不脱离前提和结论所涉及范围的直接证明。每一个捷径都可以被还原为漫长而平直的路径。这听起来很专业，但它为自动化证明搜索提供了重要基础：无切证明遵循子公式约束，能够限制需要考虑的公式范围。不过，它并不保证搜索空间普遍可控——一阶逻辑有效性不可判定，切消去也可能使证明变得极其冗长。通过正文提到的柯里-霍华德对应，切消去还连接到程序如何通过简化进行计算。根岑的这种形式记录方式，就是我们在第五乐章中将要谈到的证明助手的远祖。

第二部分

常见非形式谬误

正文给了你两种伟大的「形式谬误」——肯定后件和否定前件，它们有着破碎的骨架。但你在现实中遇到的大多数糟糕推理都是「非形式谬误」：形式没问题，内容在耍诈。自古以来，人们就开始对这些谬误进行分类（亚里士多德专门写过一篇论文《诡辩驳议》，详述了论辩中的各种肮脏手段）。掌握它们的名字是一种真正的认知升级——一旦你能给一个谬误贴上标签，你就再也无法对它视而不见。这里有一份针对最常见谬误的实地指南。

有两类谬误直接连接到第 4 日的概率论。赌徒谬误 (gambler’s fallacy)认为连续出现红色后，下一次出现黑色的概率必然升高；但独立事件不会因过去结果而改变概率。基础概率谬误 (base-rate fallacy)则是在解释证据时忽略先验比例。患病率极低时，即使检测准确率很高，假阳性也可能超过真阳性。二者都说明，直觉判断需要借助形式化概率工具校正。

第三部分

自指悖论与形式系统

正文顺带提到了罗素悖论，它是那封击碎了弗雷格毕生事业的信。但悖论在逻辑学中并非只是趣闻——它们是压力测试，是机器失灵并迫使设计重组的地方。曾有两次，一个简单的自指句子彻底摧毁了一个地基。理解其背后的「原因」，就是理解逻辑的构成材料。

说谎者悖论

从最古老的开始。考虑这个句子：「这句话是假的。」它是真的吗？如果它是真的，那么它所说的话就成立——所以它是假的。但如果它是假的，那么它所说的话就不成立——所以它是真的。这个句子在真与假之间无休止地翻转，永远无法安顿。这就是说谎者悖论 (Liar paradox)。古希腊人早已知晓它（克里特人埃庇米尼得斯的「所有克里特人都说谎」便属同类），它也绝非文字游戏。它表明，看似无辜的「真」这一概念，一旦与句子的「自指」能力结合，就会产生矛盾。阿尔弗雷德·塔斯基在 1930 年代得出了一个激进的认识：任何语言都不能一致地包含其自身的完整真值谓词。要讨论一种语言中句子的真值，你必须攀升到更高的元语言 (metalanguage)——真值永远要从更高一层来审视。（这也是为什么本课程中反复出现的动作是将「事物」与「关于事物的讨论」分开，这种层级阶梯我们在第 1 日的主观/客观划分中就已感受到。）

罗素悖论

现在来看那个真正击中弗雷格体系要害的悖论。弗雷格的地基建立在一个宽泛的假设之上：任何你能表述出的属性都刻画了一个「集合」——即所有具有该属性的事物的集合。听起来无懈可击。罗素询问了一个特殊的属性：不属于自身。大多数集合都不是其自身的成员（所有茶杯的集合本身并不是一个茶杯）。那么请考虑 R，即所有不属于自身的集合构成的集合。R 是 R 的成员吗？如果 R 是其自身的成员，那么根据其定义，它必须不是——矛盾。如果 R 不是其自身的成员，那么它符合 R 的成员资格定义，所以它是——矛盾。无论哪种情况，系统都会爆炸。理发师版本的比喻更为生动：在一个村庄里，理发师只给那些不给自己刮胡子的人刮胡子，那么谁给理发师刮胡子？1902 年，就在弗雷格巨著第二卷即将付梓之际，罗素将此寄给了他。弗雷格的回信是思想史上最优雅的灾难告白之一：「当工作结束时，发现地基动摇了，这对于一个科学家来说，大概没有比这更令人不悦的了。」地基确实动摇了。

解决方案及其代价

你如何从一个句子里拯救逻辑？罗素给出的答案，是与阿尔弗雷德·诺思·怀特黑德合著的宏篇巨著《数学原理》（Principia Mathematica, 1910–1913）。他提出了类型论 (theory of types)：将对象安排在严格的层级中——底层是个人，上层是人的集合，再上层是集合的集合——并禁止任何集合引用自身。语法规则直接将「R 是 R 的成员」判定为无意义，就像「数字七是蓝色的」一样无意义。通过分层，悖论被消除了。《数学原理》严谨到需要数百页的推导才能证明「1 + 1 = 2」（当证明终于到来时，书中还带了一句冷幽默：「上述命题偶尔是有用的」）。它是一座丰碑，也是一个警告：绝对严谨的代价可能是几乎无法阅读。

层级类型的思想并未在 1913 年消亡。1970 年代，佩尔·马丁-洛夫将其剥离了哲学包袱并重构，这便成为了 Lean、Rocq 和 Agda 等证明助手的逻辑基础。罗素为抵御悖论而修筑的防御墙，在六十年后，成为了告诉计算机什么是「证明」的理想架构。逻辑最严重的危机，播下了它现代最强大的工具的种子。

多值逻辑与其他方案

还有一个基础性的震颤，而且是个迷人的震颤。正文在非经典逻辑中列举了模糊逻辑和多值逻辑，但跳过了第一个严谨的多值逻辑 (many-valued logic)是如何诞生的故事。1920 年，波兰逻辑学家扬·卢卡谢维奇正在苦思冥想亚里士多德曾提出的一个问题：海战问题。「明天将有一场海战。」这句话在今天是真的还是假的？如果它已经是真的，那么未来似乎已被注定，自由意志荡然无存；如果已经是假的，那么海战就是不可能的。亚里士多德为此苦恼不已。卢卡谢维奇的大胆举动是拒绝承认这句话现在必须要么真要么假——他为开放的未来引入了第三个真值：「可能」或「不确定」。这个看似哲学的问题，后来长成了整个多值逻辑领域，它也是如今运行在你相机自动对焦系统中的模糊逻辑的数学鼻祖。一个关于命运的问题，被问了两千年，最终变成了一个工程分支。

第四部分

形式系统与可计算性

这是一个看起来像是玩笑、实则触及本质的谜题。它由路易斯·卡罗尔（是的，就是《爱丽丝漫游奇境记》的作者，他的日常身份是牛津大学逻辑学家查尔斯·道奇森）于 1895 年发表，题为《乌龟对阿喀琉斯说了什么》。全文仅四页，以对话体写成，却困扰了逻辑学家一百多年。

阿喀琉斯掌握了一个有效论证。两个前提分别是 A：「凡等于同一事物者，彼此相等」；B：「这两个量都等于同一个第三者」。结论 Z 是：「这两个量彼此相等」。乌龟以令人抓狂的礼貌同意 A 和 B 为真，也同意论证有效。但它拒绝接受 Z。为什么？因为它说，要从「A 和 B 为真」推导到「因此 Z」，你必须依赖某种进一步的规则——称之为 C：「如果 A 和 B 为真，那么 Z 为真」。阿喀琉斯说，好吧，那我们也承认 C。乌龟愉快地照做了——但依然不接受 Z。因为现在，要从 A、B 以及 C 推导到 Z，你还需要另一条规则 D：「如果 A、B 和 C 为真，那么 Z 为真。」以此类推，永无止境。每当阿喀琉斯试图通过将其写成显式前提来夯实推理规则时，乌龟都会要求一条新规则来为该前提提供授权。前提列表无限增长，而 Z 永远无法抵达。

「以此类推。你看，阿喀琉斯，我们现在正在进入一个没有尽头的推论序列。」

乌龟发现了一个深刻的真理：一个推理规则 (rule of inference)不能被简化为一个前提。从前提向结论迈出的那一步——推理的实际行动——本身并不是论证中的另一个前提；如果你试图将其变成前提，就会触发无限倒退。推理需要某种超出显式陈述的东西：一种「行动」的意愿，即去实际应用规则，而不仅仅是观察对规则的描述。由此可见，逻辑并不只是把越来越多的内容写在纸上；它的核心必须包含一个动作——「去做」，而不仅仅是「去说」。

你以前见过这种形状。在第 1 日，阿格里帕三难表明，每一条辩护链条要么永远倒退，要么循环，要么停在某个未经辩护的地方。卡罗尔的乌龟是穿着不同衣服的同一个骨架：任何试图为推理行动本身正名的尝试都会陷入无限倒退。这两个谜题遥相呼应，因为它们指向同一个主题——推理必须落地于某些不再是推理的东西。对于辩护，那块地板是第 1 日的「基础信念」或「可靠过程」；对于推理，它是应用规则的原始能力。两者都告诉我们，一个心智或一台机器，不能仅靠显式内容运行。在最底层，必须有一个纯粹去「执行」的东西。

头顶的天花板

正文展示的前沿——证明助手以零容错方式验证数学——自然引发了一个问题：我们是否终有一天能将所有数学形式化，将每一个真理都转化为机械检查，从而消除不确定性？这是弗雷格和罗素追求的目标，但现在我们知道，这一目标存在已被证明的界限。1931 年，25 岁的奥地利人库尔特·哥德尔证明了，任何一致、可有效公理化且足以表达基本算术的形式系统都不完备：有些算术命题在体系内既不能证明，也不能反驳。第二不完备定理进一步说明，如果这类体系是一致的，它就不能只凭自身资源证明自身的一致性。不存在一个同时一致、可有效公理化、完备且能自证一致性的算术形式化体系。这并非因为我们尚未建成，而是因为它不可能存在。

这是针对第五乐章的巨大平衡力，我们将在第 28 日用一整天来展开它。现在，请将这种张力像和弦一样留在脑海中：程序化证明强大得超乎想象，验证了人类无法手工检查的事物——同时，任何此类系统对其自身所能提供的确定性都有着坚固的、已被定理证明的极限。证明助手是一个在笼子里运作的宏伟工具，而哥德尔精准地测量了那些栅栏。请同时保留这两个部分。成就与极限是同一主题的两面——你可能已经注意到，这正是整个课程反复出现的形状。

第五部分

从形式化证明到机器核查

正文介绍 Lean 和 AlphaProof 时，仿佛它们是凭空出现的。事实并非如此。机器证明背后有着六十年的背景故事，其中包含了一些现代数学中最具哲学冲击力的时刻——在这些时刻，数学共同体不得不决定，一个没有人能完全手工验证的证明，是否依然算作一个证明。这正是前沿地带脚下的深厚历史。

两项奠定基础的定理

首先，是一份基础性的保证，它使得机械化逻辑变得值得信赖。对于标准的一阶逻辑，有两项伟大的元定理成立。可靠性定理 (soundness)：任何你可以利用规则「证明」的东西，在每一个模型中实际上都是「真」的——规则从不撒谎。完备性 (completeness)（由同一位哥德尔于 1929 年证明，这是一个比他后来的成名作温和得多的定理）：任何在每一个模型中为「真」的东西，都「可以」利用规则被证明——规则从不遗漏。这两者说明，在标准一阶逻辑中，证明规则与模型论语义可以严格对应。但 Lean 这类证明助手的信任基础并不只是这些一阶逻辑定理：它依赖小型内核、类型论基础、所采用的公理，以及形式化是否忠实表达了原问题。机器核查证明的核心优势在于：每一步都必须由内核检查，错误步骤无法蒙混过关。

引发争论的结果

第一次地震发生在 1976 年。四色定理 (Four Colour Theorem)——即任何地图只需四种颜色就能染色，使接壤区域不重色——自 1852 年以来一直困扰着数学家。伊利诺伊大学的肯尼斯·阿佩尔和沃尔夫冈·哈肯终于攻克了它，但他们的证明采用了一种史无前例、且在许多人看来惊世骇俗的做法：它将问题简化为近 2,000 种特定构型，然后利用计算机不知疲倦地逐一检查。没有人类曾验证过，或者说能够可行地手工验证所有这些案例。这算是一个证明吗？哲学家和数学家们炸开了锅。传统观念认为，证明应该是人类心智可以跟随并被说服的推理链条；而这更像是对硅片及其运行程序的某种信仰。伊利诺伊大学数学系带着一丝示威意味，开始在邮戳上盖上「四色足矣」。数学这一学科跨过了一个永远无法回头的门槛。

这种疑虑持续了数十年——直到证明助手的到来。2005 年，乔治·贡蒂尔在 Coq 证明助手中将整个四色定理形式化，将整个论证（包括计算机检查的案例）还原为由微小可信内核验证的步骤。1976 年那场看起来像盲目信仰的行为，在 2005 年变成了一个被零容错检查过的定理。机械化不仅仅匹配了那个有争议的证明，它「救赎」了它。

机器辅助解决的猜想

接着是 1996 年，一个正文暗示过但未详述的里程碑：自动化证明器第一次基本上靠自己解决了一个著名的未解问题。罗宾斯猜想 (Robbins conjecture)——这是一个提出于 1930 年代的问题，关于一组简单的代数方程是否足以定义布尔代数——曾让该领域最顶尖的高手折戟六十年。塔斯基本人也曾尝试并失败。1996 年 10 月 10 日，由阿贡国家实验室的威廉·麦丘恩编写的名为 EQP 的程序，在经过约八天的搜索后找到了证明。它登上了《纽约时报》的头版。麦丘恩给当时 81 岁的赫伯特·罗宾斯打电话，告诉他他的猜想终于被解决了——被一台机器。

但这里有一个让它成为完美寓言的转折。正如一位逻辑学家所说，EQP 产出的证明是「一个没人能看懂的计算机生成的证明」。它是一串生硬的代数替换序列，其中一些替换如此违背直觉，以至于人类做梦也想不到。它没有提供任何洞察——没有关于定理「为什么」为真的故事，只是一个无可辩驳的「它是真的」认证。这个自此一直困扰着机器证明的问题，在 2026 年的 AI 证明器面前被磨得更加锋利：如果一台机器给了你一个你无法理解的严密证明，你是否获得了「知识」，还是仅仅获得了一个裁决？数学一直从证明中追求两样东西——确定性以及理解。现在，机器可以在理解缺失的情况下交付前者。（这是第 1 日关于「正确但未以正确方式与真相相连的信念」这一忧虑的直系后裔。）

一份经过多年核查的证明

这个模式在开普勒猜想 (Kepler’s conjecture)的故事中规模更大地重演了。1611 年，那位也曾给出行星轨道的数学家约翰内斯·开普勒断言，菜贩堆放橙子的方式（「面心立方」堆放）是球体排布的最致密形式。托马斯·黑尔斯在 1998 年证明了它，但证明是一段长达 300 页且严重依赖巨量计算机计算的论证。《数学年刊》（Annals of Mathematics）的十二名审稿人努力了数年，最终给出了一个该期刊从未发布过的裁决：他们「99% 肯定」证明是正确的，但无法完全验证计算机部分。百分之九十九。对于一个以确定性为全部承诺的数学证明来说，那百分之一令人无法释怀。

黑尔斯的回应是向怀疑宣战。他启动了 Flyspeck 项目（这个名字是「开普勒形式化证明」的俏皮缩写），旨在将整个证明在证明助手中形式化，让没有任何计算是不可信的。一个国际团队耗时十余年，终于在 2014 年完工，他们结合使用了 HOL Light 和 Isabelle 系统，并于 2015 年发布了官方报告。这个悬而未决 400 年、在 1998 年只有「99% 肯定」的橙子堆放问题，终于成为了一个完全由机器验证的定理。已确立

• 1929 · 基础保证哥德尔完备性定理。 在标准一阶逻辑中，语义有效性与形式可证性能够精确对应；这为一阶逻辑的程序化证明提供基础。现代证明助手还依赖各自的内核、基础理论、公理与形式化质量。
• 1976 · 争议四色定理（Appel 与 Haken）。 约 2,000 个案例由计算机检查；这是第一个人类无法手工验证的重大证明。「四色足矣」。
• 1996 · 孤独的机器罗宾斯猜想（McCune 的 EQP）。 一个自动化证明器在 8 天内解决了一个有着 60 年历史的悬案——证明过程「无人能懂」。
• 2005 · 救赎四色定理形式化（Gonthier，Coq）。 1976 年那场对程序的盲信，变成了内核验证过的定理。
• 2014 · 400 年的终点开普勒猜想形式化（Flyspeck，HOL Light + Isabelle）。 黑尔斯那份「99% 肯定」的证明，变成了完全由机器验证的证明。
• 2024–26 · AI 转向AlphaProof 及其后。 证明内核内部的神经搜索——正文已提及，下文将深入探讨。

机器如何搜索证明

有必要揭开这些系统工作的黑盒，因为正文将证明助手视为某种黑箱。这里实际上有两项截然不同的工作，混淆它们是一个常见的错误。证明检查器 (Lean, Rocq, Isabelle) 仅仅是在其内核中步步为营地「验证」你提供的证明——它是一个怀疑论者，而非发明家。而证明搜索器或自动化定理证明器（如 EQP 或现代工具）则试图从零开始「寻找」证明。搜索中最困难但也最实用的一种形式是听起来很不起眼的SAT 求解器 (SAT solver)。给定一团混乱的真/假约束，它会狩猎出一组能同时满足它们的赋值。这就是布尔可满足性问题，而且（正如我们在第 29 日将看到的）它坐落在计算机科学中P vs NP 问题的核心。尽管 SAT 在最坏情况下计算上难处理，现代 SAT 求解器却能例行公事般地啃掉包含数百万变量的问题，它们悄无声息地驱动着芯片设计、软件验证和物流规划。2016 年，一个解决名为「布尔毕达哥拉斯三元组问题」的染色问题的 SAT 证明，产出了一个长达 200 TB 的凭证，这是当时人类历史上最大的证明。这是一个你永远无法打印、更别说阅读的证明，但它的每一行都可以被机械地检查。卡罗尔的乌龟想必会对它感慨万千。

带有形式核查的 AI 证明器

这让我们回到了现在，以及正文中 AI 故事的深层版本。2024–2026 年真正的边疆是两个天生一对的事物的结合：神经网络「猜哪一步值得一试」的天赋，以及证明内核拒绝接受不符合形式规则的步骤。有几个研究线索值得记住它们的名字。自动形式化 (autoformalization)——即将用普通英语撰写的数学文本自动翻译成机器可以检查的形式化陈述——是每个人都在竞相拓宽的瓶颈，因为世界的数学知识几乎全是以散文形式存在的，而机器只能验证已被形式化的内容。像 LeanDojo 这样的工具将证明助手变成了 AI 的训练环境。而正文描述的 AlphaProof 系统，正是通过「将约一百万个问题自动形式化为 Lean 语言，并针对内核的裁决进行训练」来运行的。正如 DeepMind 所言，在经过核查的形式推导中「无需担心幻觉」——无效的形式步骤无法通过编译。

一份比正文更直白、更可信的账单：

• 已确立：AI 已经达到了竞赛级别的竞技水平；AI 辅助的形式化正在真切地加速；2026 年 5 月，OpenAI 的一个内部模型生成了埃尔多什单位距离猜想的反例，并由人类数学家核查、整理并阐释。内核核查系统不会接受违反其形式规则的推导。因此，通过核查意味着定理相对于形式陈述、所用公理和内核成立；形式化是否忠实表达原本的非形式主张，则是另一个问题。这一有明确范围的保证才是关键：机器学习的创造性搜索可以与机械证明核查结合。
• 有前景：2025–26 年的预印本描述了 AI 智能体在 Lean 中解决了一些此前未解的（尽管是狭窄且专业化的）问题；单位距离结果则表明，自主数学发现有时已经能进入被接受的研究层面。这些成果新鲜、重要，但仍参差不齐。保持关注，但暂且不要被宣传语带跑。
• 有争议／炒作风险：任何宣称 AI 已经「解决了数学」或让数学家失业的说法。一个里程碑式反例并不等于通用数学智能；竞赛题也仍只是有着已知简短答案的一小部分。正如正文所提醒的：即便是在 2025 年的「金牌」水平，依然有几十名人类少年得分更高。

纵贯这六十年——从阿佩尔和哈肯那张有争议的地图，到没人读得懂的罗宾斯证明，再到在 Lean 内核中搜索的 AlphaProof——都贯穿着同一个安静的想法，也是正文结尾的那个：亚里士多德想要一条不容置疑的推理链条。我们终于造出了一台能够逐行执行这一标准之形式版本的机器，其结论相对于指定内核与公理成立。而我们仍在发现那台机器引发的新问题：一个人类无法阅读的证明，是否能被称为「理解」；以及那份经过形式核查、却没有洞察力的确定性，是否真的是数学家们一直以来真正追求的东西。

简报 I

开放权重证明器的发展

正文中的 AI 证明故事停在了 AlphaProof：一个躲在公司围墙后、解决每个问题都需要耗费数日算力的封闭系统。自那以后，该领域出现了 AI 界少见的开放趋势：若干证明器开放了权重，而且能力提升很快。到了 2025 年，一些开放权重证明器已能在个人级硬件上运行，并在形式化、机器检查的 Lean 语言中解决奥数级数学问题。这是一场静悄悄的地震。

要跟上它的节奏，你需要了解计分板。机器证明器是根据共享的基准测试（benchmarks）进行排名的——这是一组用来比较不同系统的固定题目。其中有三个至关重要。miniF2F（2022 年推出）包含几百道奥数级别的题目，直到最近还是行业标准；现在它已趋于饱和，顶尖系统的得分已接近天花板。PutnamBench（2024 年）难度更高——题目选自臭名昭著的普特南（Putnam）本科生数学竞赛，人类得分的中位数通常是零。FrontierMath（2024 年）按难度分层，范围从有挑战性的大学数学一直延伸到可能让专家耗费数日的研究级问题。它的分数取决于难度层级、数据集版本和评测规程，不能用一个百分比概括整个基准。随着一个基准测试达到饱和，领域内就会建立一个更高的基准。

现在来看看那些不断攀登的系统。在 2025 年，两款开放权重证明器重塑了人们的预期，而第三款则冲入了奥数金牌水平。

有两点值得强调：一点令人振奋，另一点用来限制结论。令人振奋的是：一个 320 亿参数的模型——小到足以在严肃的业余研究者或小型实验室拥有的个人级硬件上运行——现在已经能与一年前需要数据中心支撑的系统平起平坐。能力在体积和成本上都在飞速塌缩。而限制结论的那一点隐藏在 「Pass@k」 这个术语中。当一篇论文报告 「miniF2F 达到 88.9%」 时，通常意味着模型被允许针对每个问题进行数千次尝试，并至少成功了一次。「机器解决了它」可能悄悄意味着「八千次尝试中有一个编译通过了」。这不算作弊——对于形式化证明，只要有一个编译通过的证明就是证明，无论之前经历了多少次失败——但这与一个因为「理解」了题目而能一次性做对的人类是完全不同的。请记住这两个事实：证明器确实在迅速变强，同时标题中的百分比也美化了它们。

简报 II

机器辅助发现新的数学构造

证明一个已知的定理是一回事。而发现一个新的数学对象——构造出一种人类从未写下的结构——则是另一回事。2023 年，一台机器做到了这一点，其方式非常值得研究，因为它极易被误读。

该系统名为 FunSearch，由 Google DeepMind 开发，于 2023 年 12 月发表在《自然》杂志上。它的设计既优雅又带点自谦。选一个棘手的数学问题，目标是寻找某类对象的最优构造。让大语言模型编写能生成候选构造的小程序。根据输出结果的好坏为每个程序评分。保留优胜者，将它们反馈给模型进行变异和改进，并不断循环——这是一种进化搜索，LLM 是变异的来源，而一个快速、简单的评分器则是裁判。目标是 盖集问题（cap set problem），这是组合数学中一个著名的难题，菲尔兹奖得主陶哲轩曾称其为自己的心头好。FunSearch 在 8 维空间中找到了一个大小为 512 的盖集——超过了此前保持了 20 年之久的记录 496，让停滞不前的下界第一次向上移动。

这是一个真实的、可验证的、全新的数学结果，值得一个 已确立 的评价。但现在请看其细则，因为细则才是全部教训所在。首先，这种情况很罕见：在 140 次实验运行中，只有 4 次找到了大小为 512 的集合——在大量尝试中，系统只有少数几次找到了成功构造。其次，更奇怪的是：语言模型从未被告知它在处理什么问题。它看到的只是一个抽象的评分函数和编写更好程序的要求。它没有「盖集」的概念，不懂数学，也不知道自己正在创造历史。这种「洞察力」其实存在于循环中——模型盲目的生成流畅性与评分器判别优劣的能力相结合——而非产生于任何机器理解的瞬间。计算机科学家欧内斯特·戴维斯在评论这一结果时强调了这一点：真正有趣的是「人机反馈结构」，而非自主的 AI 洞察。随后，人类数学家乔丹·艾伦伯格观察了 FunSearch 的产出，发现程序误打误撞进了一个对称结构，并利用人类的观察进一步推高了边界。机器搜索出了构造，人类从中辨识出数学结构。

这种模式随后被放大。 AlphaEvolve（DeepMind，2025 年）将 FunSearch 的理念推广为更广泛的「进化编程智能体」。2025 年 11 月的一篇论文——「大规模数学探索与发现」，陶哲轩本人也是作者之一——将其应用于分析、组合、几何和数论领域的 67 个问题，重新发现了已知的最优点并改进了一小部分。已确立 作者本人的准确表述，正是这篇简报的核心结论：这些系统正在以超人的规模和速度进行 搜索与优化。它们不是在进行「证明」，也不是在进行「理解」。它们是一种新型且强大的数学望远镜——而望远镜本身发现不了任何东西，它只是让数学家看得更远。

简报 III

埃尔多什问题：如何核对新闻标题

如果你想找一个故事，能教会你本课程的核心技能——区分真实主张与听起来真实的主张——那么 2025 年到 2026 年冬季公开上演的这场「AI 与埃尔多什问题」风波是不二之选。它包含一个宣传高峰、一次剧烈修正，以及随后一个宁静且真正有趣的真相。请观察这三个节拍。

背景：保罗·埃尔多什，这位四处游历的匈牙利人，一生提出的问题可能比历史上任何人都多。他留下了数百个悬而未决的问题，目前由数学家托马斯·布鲁姆维护的一个公开数据库进行归档。对于那些想要证明实力的 AI 实验室来说，这些问题是不可抗拒的目标。

第一阶段：高调发布

2025 年 10 月，OpenAI 的重要人物大张旗鼓地宣布，GPT-5 已经 「找到了 10 个（！）此前未解的埃尔多什问题的答案」，并对其他问题取得了进展。这个数字迅速传遍互联网，听起来像是机器开始进行真正的数学研究的时刻。有争议／炒作风险

第二阶段：独立核查

修正来得很快，且出自最权威人士之手。维护数据库的托马斯·布鲁姆称这一说法是 「极具误导性的陈述」。这些问题并不是被 GPT-5 「解决」的，而是几年前就被人类解决了，只是布鲁姆还没来得及录入论文——而模型完成了一项真正有用但完全不同的工作：找到了这些现成的论文。在他数据库里的「未解」，仅仅意味着「我个人还不知道有论文解决了它」。其中最典型的问题 #339，大约在二十年前就已经尘埃落定。GPT-5 展示的是卓越的「文献搜索」能力，而非数学发现。甚至竞争对手实验室的负责人哈萨比斯也称这一插曲「令人尴尬」。OpenAI 随后发表的论文悄悄地重新界定了结果：是检索，而非证明。

机器并没有回答问题。它只是找到了别人已经给出的答案——而一份公关稿却把图书管理员包装成了数学家。

第三阶段：保留可靠结论

然而。拨开夸张包装，等待几个月，同样的努力中确实浮现了一些真实的成果——这正是为什么这是一个精彩的故事，而非简单的辟谣。到 2026 年 1 月，陶哲轩谨慎地报道称，极少数埃尔多什问题确实以一种看起来确实是新的方式被解决了。他写道，问题 #728「由 AI 基本上自主地解决（在获得一些反馈后……），符合问题精神……据我们所知，该结果尚未在现有文献中复现」。随后又有几个问题效仿此法，其中一些通过名为 Aristotle 的系统在 Lean 中进行了形式化验证，并得到了陶哲轩本人的认可。有前景

但请注意陶哲轩——一位在一线工作的数学家，而非营销部门——是如何界定它的。他的框架正是本课程试图为你建立的「校准思维」典范。他强调，这些是 「最容易摘的果子」（lowest-hanging fruit）。埃尔多什问题的难度差异极大，跨越数个数量级；「未解」标签「始终是暂时的」；而且报道存在严重的偏差，因为失败从未被公布——该工具已经「悄悄地应用到了相当比例的现存埃尔多什未解问题上，但并无显著成功」。成功是真实的，值得庆祝。但它们也是那一堆问题中最简单的，是在人类反馈的循环中解决的，且在文献中已有非常相近的结果。用陶哲轩优美的原话来说，机器正在「清理那些最容易摘的果子，并分离出那些真正困难的问题」。

• 2025 年 10 月 · 高峰「GPT-5 解决了 10 个未解的埃尔多什问题。」 由 OpenAI 人物发布；被广泛转发为研究突破。有争议／炒作风险
• 2025 年 10 月 · 修正「极具误导性的陈述」——托马斯·布鲁姆。 这些问题多年前已被人类解决；AI 只是找到了现成论文。哈萨比斯：「令人尴尬」。
• 2026 年 1 月 · 真相埃尔多什 #728「基本上自主」解决，文献中未见。 随后还有几个案例，部分经过 Lean 验证并被陶哲轩接受——但属于「最容易摘的果子」。有前景

这一课并不是说「AI 数学全是假的」——第三拍是真实的，而且很可能是某种宏大趋势的前哨。这一课告诉我们，同样的底层事件，在 10 月产生了一个极其错误的头条，在 1 月产生了一个严谨的真实声明。而分辨它们的唯一方法就是追问：说话者是谁，「已解决」和「未解」究竟意味着什么，以及结果是否经过验证。这就是「前沿校准器」在实时新闻中的典型用法。请掌握这套方法；在具体的题目编号被忘却后，你依然会需要它。

简报 IV

这些系统是否真的在推理？

在基准测试分数和头条新闻之下，隐藏着一个尚未解答的问题，而且持不同立场的严肃研究者都承认，这个问题仍未解决：当一个模型给出一连串看起来合理的步骤并得出正确答案时，它是在进行 推理——还是在对数以十亿计的案例进行一种极其精妙的模仿与模式匹配？这是第 1 日那个问题的现代机械化版本：输出真实主张的系统是否真的知道什么。在 2024 到 2025 年间，这引发了该领域最激烈的实证交锋之一。

支持「模式匹配」的证据

导火索是苹果公司机器学习团队的两篇论文。第一篇是 GSM-Symbolic（发表于 2025 年 ICLR 会议），进行了一个精妙且简单的实验。拿模型能轻松应对的小学数学应用题，只改变其中的 数字和姓名——推理逻辑完全不变——观察得分。结果分数出现了波动，这如果模型真的理解方法，本不该发生。接着，他们做了更残酷的一步：在题干中加入一个 在主题上相关但在逻辑上无关 的句子。表现 轰然塌缩——跌幅高达 65%。加入一句看似相关、实则无关的干扰信息后，最强模型的得分从 94.9% 瞬间掉到了 63.0%。作者的结论很直白：模型「无法进行真正的逻辑推理」；它们只是「从训练数据中复制推理步骤」。第二篇论文《思考的幻觉》（2025 年 6 月）更进一步，指出在汉诺塔等受控谜题上，最新的「推理」模型在超过一定复杂度后会出现「准确率全面塌缩」——而且诡异的是，随着问题变难，模型开始变得 不那么努力 了。

支持更复杂解释的论据

反驳也随之而来。一份广泛流传的回复——半开玩笑地署名了一位 AI 合作作者——认为苹果的实验结果在一定程度上是 实验误差造成的假象：有些「失败」仅仅是因为模型在回答中途触及了输出长度限制，而有些被判为失败的谜题实例 本身在数学上就是无解的，所以任何系统都不可能做「对」。西班牙一个研究小组的独立复现（2025 年 9 月发布）得出了一个折中的结论：没错，部分剧烈的塌缩确实是由于输出限制造成的，但并非全部；即使复杂度只是适度上升（例如在八个圆盘时），模型确实会陷入挣扎。真相正如本页常态：并非任何一个头条所言。

需要警惕的反向证据

还有第三个发现，虽然不如「苹果之争」出名，但可能更重要，因为它触及了信任机器推理的根基。当模型「展示它的思考过程」——即现在随处可见的、在给出答案前叙述步骤的「思维链」时——我们自然会假设这种叙述 就是 它的推理过程。Anthropic 对齐团队的研究（2025 年）表明，事实往往并非如此。他们测量模型给出的理由在多大程度上忠实反映真正驱动答案的因素，发现其 忠实性（faithfulness）低得惊人：一个领先模型约为 25%，另一个约为 39%。当研究人员向模型提供暗示，且模型确实使用了该暗示时，模型通常 闭口不谈——而是构建了一个听起来合理的「马后炮」解释。换句话说，思维链并不是透视机器真实过程的可靠窗口。它有时只是模型为自己通过其他手段得出的答案编造的一个故事。

请仔细思考这对 AI 「证明」意味着什么。如果一个系统交给你一个步骤详尽的论证，而这些步骤与它得出结论的真实路径 并不 一致，那么这个解释就只是装饰性的——你又回到了第 1 日遇到的盖梯尔担忧：结论可能是正确的，但其给出的理由与它正确的原因毫无关系。这就是为什么简报 I 中经过 Lean 验证的证明器如此重要。在整个前沿领域中，那是唯一可以完全避开「推理是否真实」这一问题的角落——因为内核不看故事，它只检查证明。当你无法信任解释时，请验证结果。整个前沿领域最终都会回到这一句话上。

简报 V

基准分数必须标明版本

本页的主张最终都依赖基准测试结果，但只给出基准名称，并不能确定一次具体、稳定的测试。可用的成绩应当同时标明数据集版本与难度层级、模型版本或快照、工具与脚手架、推理或尝试预算，以及计分规程。FrontierMath 正好说明了原因。

2024 年 12 月，OpenAI 报告称，当时尚未发布的 o3 在包含 180 道题的 FrontierMath_11-26-24 上取得了 25.2%。Epoch 目前的模型页面则列出：正式发布版 o3 在 FrontierMath Tiers 1–3（v1，旧版）上为 18.7% ± 2.3%，在 Tier 4（v1，旧版）上为 2.1% ± 2.1%。这些并不是同一次实验的重复：模型版本和题目集合不同，现有报告也不能证明脚手架、推理设置、尝试预算或计分规程完全一致。因此，后两个数字既没有复现，也没有否定 25.2% 的公告。依赖评测规程

数据治理方面另有一个合理的疑问。OpenAI 委托 Epoch 制作了 300 道核心题和 50 道 Tier 4 题。Epoch 表示，OpenAI 拥有这些委托制作的题目，并可访问截至 FrontierMath_12-04-24 的全部题目和答案。后续版本才加入明确的留出集：FrontierMath_02-28-25 留出了 53 道核心题的答案，Tier 4 则留出了 50 道题中的 20 道。Epoch 在 o3 公告前已经公开双方的合作关系，但后来承认，当时没有明确说明所有权和数据访问条款，许多出题者也不了解这些细节。这种信息不对称足以要求更醒目的披露和独立留出评测，但它本身并不能证明所报告的成绩是捏造的。

版本变化也会影响比较。2026 年 6 月 12 日，Epoch 发布 FrontierMath v2，修正了 42% 题目中的问题。修订基准是正常且有益的维护工作，但 v1 与 v2 的成绩因此不能在不加说明的情况下直接比较。稳妥的结论应当更窄：25.2% 是一个模型快照在某个具名版本和一套评测条件下的报告结果。若要概括 o3 更广泛或当前的能力，需要在版本匹配、条件公开的评测中重新测量。

简报 VI

其他重要进展

AI 证明的故事占据了大部分注意力，但自 2020 年以来，另外四个前沿领域也取得了实质性的进展，虽没那么喧嚣，但在某些方面却更为坚实。它们完善了全景图，其中一些在长远看来可能比今年的排行榜更有意义。

连续统假设重回视野

数学中最深层的根基问题——康托尔的 连续统假设（Continuum Hypothesis），即在整数和实数之间是否存在某种大小的无穷大——曾被哥德尔和科恩证明是与标准公理 独立 的：你既不能证明它为真，也不能证明它为假。几十年来，这看起来像是盖棺定论了。但 W·休·伍丁多年来一直在构建一种他称之为 终极 L（Ultimate L）的备选架构。最近的研究（2024 年）出现了一个惊人的逆转，结果表明，如果 他的核心猜想成立，由此产生的自然公理将使连续统假设的结果为 真——推翻了他早先认为其为假的倾向。已确立 作为严肃的数学，但这套猜想依然悬而未决。其他人（尤其是乔尔·大卫·哈姆金斯）则认为这个问题根本没有唯一答案，存在一个由同样合法的集合论组成的 多重宇宙。关于无穷大的、有着两千年历史的疑问，竟然依然活跃。

一个证明可以自我计算的根基

除了将数学建立在集合之上，另一种选择是将其建立在 类型 和 空间 之上——这就是 同伦类型论（HoTT）及其「单价基础」计划。它将「相等」视为一种路径，从而将几何学引入了根基。其最新的变体——立方 类型论，终于为该计划提供了长期缺失的东西：计算 能力。2023 年，研究人员利用 Cubical Agda 形式化地确立了一个关于球面同伦群的深奥事实，并在此过程中让计算机 计算 出了一个具体的数字（即 Brunerie 数），而这个数字多年来一直无法通过手工计算得出。已确立 相对于 Lean 的集合论主流而言，这依然属于小众领域，但它展示了一种全然不同的、更具计算性的数学根基方案。

用逻辑反制 AI

如果神经网络将要驾驶飞机或阅读扫描图，我们希望得到关于它们行为的 证明。现在，一个名为 神经网络验证（neural-network verification） 的子领域已经存在。利用从验证 seL4 和 CompCert（见正文）发展而来的形式化方法，名为 α,β-CROWN 等工具可以为训练好的网络提供数学保证——例如，输入的微小扰动不会导致输出翻转。目前有一个年度竞赛来推动这些工具的发展，它们正迅速成熟。已确立 这是一个巧妙的倒置：前六篇简报都在追问 AI 是否能做逻辑，而在这里，逻辑被用来监管 AI。目前本页所有成功的范式——将神经创造力与符号检查器相结合——都有一个共同的名字：神经符号 AI（neurosymbolic AI）。它被越来越多地视为通往真正可信系统的必经之路。

证明的可核查性与可理解性

最后是一个哲学而非技术的前沿，也是本页一直在徘徊的问题。一些严肃的文献——杰里米·阿维加德的《数学与形式化转向》（2024 年）、埃蒙·杜德等人关于「计算不透明时代」的知识研究——提出了一个问题：当证明变成只有机器才能检查的东西时，数学上的 理解 会发生什么？数学对证明一直有两种诉求：对结论真实性的 确定性，以及对「为什么」的 理解。机器现在在提供确定性方面表现卓越。数学家亚历克斯·康托罗维奇描绘了一个噩梦版本：一个长达百万行、经过机器验证的黎曼假设证明，它是 绝对正确 的，却又是 完全不可理解 的。这是第 1 日提到的「正确却不被理解的信念」的终极形态。这究竟是胜利，还是对学科内涵的掏空？这不是任何基准测试能解决的问题。悬而未决 这也是这篇简报留给你的思考。

轮到你了

前沿证据校准练习

你已经看过六次前沿校准器如何工作。现在请亲自动手。下面的每张卡片都是 2023 到 2026 年间前沿领域的真实主张，取自上述简报。请决定它属于哪一类——已确立、有前景 或 有争议／炒作风险——然后揭晓答案与理由。目的不在于拿满分，而在于让这种校准变成一种本能。