机器证明：从罗素的梦想到 2026

这门课回答一个问题：当新闻说"AI 证明了一个数学定理"，这件事到底是怎么发生的？它和"AI 写了一段看起来像证明的文字"有什么区别？为什么我们要相信 Lean 编译器，而不是相信某个 AI 的自述？

第 1 讲 罗素的梦：为什么 1900 年的数学家想把数学"写完"

1900 年巴黎数学家大会上，罗素和希尔伯特分别提出了同一个梦想：把全部数学写成一套有限的公理和规则，让任何一个命题是不是真的，原则上都可以靠机械推演来判定。这门课从这个梦想讲起——它为什么在那个年代出现，它吸引了当时最聪明的一批人，以及《数学原理》那三卷近 2000 页的书到底在干什么。随堂检查：《数学原理》第二卷第 362 页才证明了 1+1=2，这说明形式化证明的什么特点？

第 2 讲 哥德尔的墙：1931 年那两记闷棍

哥德尔不完备定理到底说了什么？用不超过三个例子讲清楚：为什么任何一个足够强的形式系统都一定有它证不出来的真命题，为什么系统不能证明自己的一致性。重点是理解：哥德尔没有否定形式化，他只是给形式化画了一条边界。随堂检查：哥德尔定理是否意味着"形式化证明毫无用处"？为什么？

第 3 讲 从逻辑理论家到四色定理：机器第一次走进数学证明

1956 年的逻辑理论家程序自动证明了《数学原理》第二章的定理；1976 年的四色定理靠计算机跑了 1200 机时检查 1936 种构型。这两件事分别在"机器写证明"和"机器查证明"两个方向上迈出了第一步。本讲用这两个历史节点讲清楚自动定理证明的两条路线。随堂检查：四色定理在当时为什么引发"这算不算证明"的争论？

第 4 讲 证明助手：Coq 与 Lean 怎么工作

证明助手不是让机器自己找证明，而是数学家像写程序一样写证明，机器逐行检查。本讲用一个最简单的命题演示 Lean 代码长什么样、编译器怎么报错。讲清楚 mathlib 这个开放数学知识库是怎么回事。随堂检查：为什么说证明助手的瓶颈在 2024 年以前是"写"，2024 年以后被大模型缓解了？

第 5 讲 2026 年的三桩大事：费马、渗流、OpenAI 三发现

把 2026 年 9–10 月的三桩事放在一起讲：Claude 用 11 天把费马大定理形式化；AI 在自主探索中补上渗流临界值 θ(p_c)=0；OpenAI 抛出三个新数学发现（其中杨-米尔斯相关一项仍在独立复核）。本讲重点不是背新闻，而是学会区分"重新形式化已知定理"和"从零发现新定理"。随堂检查：Claude 形式化费马大定理，和怀尔斯 1994 年证明费马大定理，是同一件事吗？

第 6 讲 可信度结构：为什么"机器可校验"是分水岭

过去一个定理被认为是真的，靠的是同行评审和声望；2026 年多了一道证据——Lean 编译器跑通。本讲对比这两种可信度结构：同行评审慢、会出错、依赖人；形式化快、不依赖声望、但只在它覆盖的范围内有效。随堂检查：为什么 OpenAI 那 722 篇手稿里会有一部分被撤回？形式化这道关在其中起了什么作用？

第 7 讲 给普通人的阅读指南：怎么判断一条"AI 数学"新闻

本讲落到可操作：以后看到"AI 证明了 XX"的标题，问三个问题——它是不是形式化证明？它是重新形式化已知定理还是从零发现？它过没过同行评审、有没有独立复核？用 2026 年 10 月 OpenAI 三个发现里杨-米尔斯那一项作为案例，练习这套判断流程。随堂检查：如果一条新闻说"AI 解决了一个千禧年大奖问题"，你在转发之前应该先查哪三件事？