先说结论

这是 Machine Learning Street Talk 围绕科学记者 Kevin Hartnett 新书《Proof in the Code》（2026 年 6 月在美国出版，节目称欧洲版当月晚些时候发行）做的一期约 94 分钟特辑。到场的不只是作者本人，还有书中三位主角：Lean 的创造者、微软研究院出身的 Leo de Moura，卡内基梅隆大学哲学家兼逻辑学家 Jeremy Avigad，以及帝国理工数论学家、MathLib 最著名的布道者 Kevin Buzzard；中间还插入了主持人早前在墨尔本采访范畴论学者 Paul Lessard 的片段。整期节目讲了两个互相咬合的故事：其一，Lean 这个为验证软件而生的工具如何被数学家「收编」，把数学证明的信任从声誉与人际关系迁到可检查的机器证书上；其二，2024 年之后 AI 证明的爆发又如何把这枚证书变成新问题的起点——被验证的证明未必证明了你想证的东西。本文依据英文自动转写整理，全部时间段（0s–5613s，共 47 段）已完整读取。

为什么需要机器读证明：从 Kepler 猜想到「没人真正读过 Scholze」

节目用两个历史案例说明数学的信任危机不是新事。Hartnett 讲述，17 世纪初开普勒在水果摊前猜想金字塔堆叠是最密堆法，此后近四百年无人能证；上世纪九十年代 Thomas Hales 与 Samuel Ferguson 把「Kepler 猜想」归约到 1762 种构型（转写另一处作 1767 个程序，两处数字不一致，疑有识别误差），靠高度优化的程序逐个验证密度不超过约 0.74。1998 年 Hales 把证明投给数学年刊（Annals of Mathematics），主持人朗读书摘（经作者许可）：审稿人看过的每一部分似乎都对，但整个证明是埋在计算机代码里的庞然大物，没人能确定这些部分如何咬合成 Hales 声称的结论；审稿拖了多年，最终「带着免责声明被接受」——Hartnett 称 editors 表态相当于「99% 置信正确」。Hales 随后转向证明助手，用 HOL Light 与 Isabelle 把自己的证明完整形式化，主持人称他因此「出了两次名」。

二十年后的版本更具冲击力。Buzzard 自述：2020 年 11 月菲尔兹奖得主 Peter Scholze 写信问他，是否「仔细读过」某条定理（转写作 Theorem 8.4，说话者本人也表示记不清编号）的证明——那是论文里约六页的技术计算，Buzzard 组织的伦敦读书会与普林斯顿、哈佛的同行的答案一样：都只读过陈述、略过了细节。Scholze 的结论是「没人真正读过我的工作」。社区随后在博客公开挑战、协作形式化，Johan Commelin（转写多作 Comelin/Comelin）找到一处简化把工期砍半，六个月后机器宣告证明成立。Buzzard 说这让 Scholze 兴奋地意识到系统「真的有用」：不仅确认了正确性，还找到了更概念化的论证，而且「终于有什么东西真正读完了它」。第二个博客帖子在社区走红，Quanta 与 Nature 相继来电——用 Buzzard 的话说，「我们到了」。

这期节目还埋了一个更扎心的注脚。Buzzard 的团队正在把数学年刊本十年发表的定理「只形式化陈述」（下详），已写成 50 条定理的陈述并将公开；公开前他们让 AI 检查了一遍，发现两类错误：一类是团队自己翻译错了；更有意思的一类是「忠实翻译了论文原话，但原话本身不成立」——作者忘了写「显然 n 至少为 3」或「该集合非空」这类默认假设。Buzzard 称他们发现至少四位菲尔兹奖得主在数学年刊证明过的定理，严格按字面读「并不为真」，专家当然知道「作者显然是想说……」。他的结论：数学这门号称完全精确的语言，实践中只跑在「99% 的精度」上，而机器提供了升到 100% 的机会。

Lean 的来历：为软件验证而生，被数学家收编

de Moura 的自述勾勒出工具的谱系。2006 年微软内部各家自造定理证明器、重复劳动严重，他造出 Z3——一个自动化定理证明器，把软件路径表达成变量组合、证明坏状态不可达，用来自动查 bug；主持人称其「为微软省了数亿美元」，还在世界 ATP 竞赛中拿了冠军。但自动化证明器能证的东西范围有限，de Moura 转向更富表达力的交互式定理证明器（ITP）：Lean 由此诞生。Hartnett 把自己的书概括为「一个为验证软件而造的工具，如何被看到潜力的数学家接管、第一次真正进入数学主流工作方式」的故事。

技术上，节目借书里的定义解释了信任的根基：ITP 由逻辑基础与一个叫 kernel 的检查器组成，kernel 验证每一步推导是否遵守逻辑规则；Lean 的策略是「小信任基」——正如 Linux 有无数 bug、但信任结论只需信任小得多的 kernel（转写此处把 Linux 误识作 Linu）。kernel 最重的罪是把假命题验成真：那会连锁放行无数假命题，直到修复前整个系统作废。历史上 Agda、Coq、Isabelle 的 kernel 都出过这类 bug；de Moura 的对策是独立检查——让用户能自建 kernel，为此 kernel 必须极小，这也是他钦佩 HOL Light 的原因。

决定 Lean 命运的是一场路线之争。Avigad 是 CMU 哲学系出身（自嘲「介于数学、计算机科学与哲学之间」的逻辑学家），2009–2010 年休假年在 Coq（转写作 Ruc，按「依赖类型论、用于形式化 Feit–Thompson 定理」的描述应为 Coq，疑为误识）里做 Feit–Thompson 定理（转写作 White Thompson）形式化，深感简单类型论的 Isabelle 表达现代数学中公理化刻画的代数结构时会「撞墙」。而 de Moura 起初倾向更简单的高阶逻辑。节目披露了 de Moura 2013 年深夜邮件的措辞：他质疑依赖类型论的必要性，因为「HOL Light 的设计最优雅」；但他也承认「重要的是有用户，我想要 Jeremy 成为用户」。最终他发邮件决定采用依赖类型论，Avigad 笑称自己「在匹兹堡家里跳了支舞」。de Moura 后来举例说这一赌注长期见效：他在微软的老同事、密码学者 Cedric Fournet 现在用 Lean，因为 MathLib「有验证密码学所需的正确抽象」。

人事的裂痕同样是书的主线。de Moura 一人扛着 Lean（「他是研究员，不是项目经理，没有工程师团队」），却被蜂拥而来的数学家的功能请求淹没；他极度自我批判，「用户喜欢它，他觉得它是垃圾」。2018–2022 年他与数学社区发生实质性决裂——书中将其部分归因于他与 MathLib 核心开发者 Mario Carneiro（转写作 Carniero/Carnero）的路线与个性冲突——独自去写 Lean 4，撂下「让我清静」的话。和解发生在西雅图联合数学会议期间：一场 de Moura 张罗的晚餐（他顺手把它变成 Avigad 的生日饭），次日在派克市场散步一下午。Avigad 回忆「过去几年像超现实」。

MathLib 这条平行线由 Buzzard 讲述，是全期最生动的部分。2017 年他陷入「中年危机」：发现自己领域的论文依赖「长者们的意见」（opinion of the elders）背书， sloppy 论文摞着 sloppy 论文，「担心自己的领域正在变成纸牌屋」。他找到的证明助手能以「超人精度」检查数学，但库里 99% 是几百年前的基础内容，甚至没有复数。于是他提了人生第一个 PR——「复数，版权所有 2017 Kevin Buzzard」——然后每周留一晚教本科生把课程「喂」给机器，因为「孩子们终于能自己上学了，我可以待到很晚」。三年后回望，「它基本学会了我们教本科生的全部东西」。Hartnett 2020 年为 Quanta 写 MathLib 报道时形容它有「谷仓共建」（barn raising）的精神：没有中央权威的众包。库的哲学被 Buzzard 讲得很清楚：只收「打磨过的、处于正确一般性的思想」，改一个基础定义会弄坏几千个文件——「我们想一次做对」。他自嘲早期营销屡屡失手：形式化 Grothendieck 的 scheme，同行集体打哈欠（「这是六十年前的老数学」）；改成与 Massot、Commelin 三人按「蓝图」清单形式化 Scholze 的 perfectoid space——Hartnett 称之为「从研究生数学直插前沿的细窄摩天楼」——才真正立住了 Lean 能做前沿数学的名声。

还有一条被验证的预言：Hales 2017 年在剑桥牛顿研究所的报告（Buzzard 通过直播观看）提出，与其让数学家翻译百页证明，不如只请他们用形式语言写下定理的陈述——陈述短、无歧义，价值却大。Buzzard 说这在 2017 年「还做不动」，七年后他写了基金申请专门做这件事：把顶级纯数期刊本十年的定理陈述译入 Lean，做了一年「完成了 20%」，预计一年后远超 20%——Hales 的愿景正在兑现。

AI 上场：从 AlphaProof 到 2026 年 9 月

AI 部分由 Hartnett 主述。2024 年 DeepMind 的 AlphaProof 沿 AlphaGo 式强化学习训练，输出 Lean 证明、由 Lean 验证，在 IMO 2024 拿到银牌级分数（题目在人类选手做完后发给它，时间与算力都不受限）。瓶颈在把自然语言赛题自动形式化：代数与数论因天然带方程与记号，约 80% 的题目能近乎完美地自动翻译；组合题「读起来像故事」，几乎无法记号化，最困难。DeepMind 最终产出数千万道 Lean 陈述的题库。2025 年 7 月，DeepMind 与 OpenAI 报告用自然语言证明达到 IMO 金牌级（谷歌成绩由 IMO 官方评分），不再依赖 Lean 验证赛题答案——Hartnett 认为两者会并存：Lean+RL 是训练引擎，LLM 的价值在于海量生成候选证明、由 Lean 快速筛出正确的那些。

对 2026 年的近期事件，节目均以「节目称」口径转述：Epoch AI 的固定预算测试中，一个预发布 OpenAI 模型证明了 Erdős 问题 126、用反例推翻问题 74，两项都经 Lean 检查，68 题里解出 2 题、其余四个模型一题未解；9 月 8 日 OpenAI 还发布了 Navier–Stokes 千禧年问题的「宣称解决」并附 Lean 形式化，但主持人补了一句「当时的情况并不理想」，未展开。更早的 2024 年 9 月，陶哲轩发起 Equational Theories 开放协作：2200 万个「哪些代数定律蕴含哪些」的问题，一个月内缩到 238 个，11 月底 138 个，次年三月底卡在最后 4 个。陶视之为「实验数学」的试点——类比现代物理的大协作产数据、与理论互补，在「来自火星的数学」里撞出新构造，比如 magma 上同调：起初称该项目「巨大得离谱的浪费时间」的上同调专家 John Baez（转写作 John Bayes）承认从未见过它。

新张力：验证过的证明，可能证错了东西

后半场的关键词是 AI 与 MathLib 哲学的碰撞。Buzzard 的观察最尖锐：MathLib 的设计原则是「找到正确的抽象、在正确的一般性下发展一切」，因为这让以后省力；而现在的 AI「根本不在乎重新设计」，看到书上的数学就直译成 Lean，「很高兴地硬耕过去」。「如果你准备好往问题里倾倒 token，我们未必需要找到正确的概念化方式。」他说 OpenAI、Anthropic「在做数学、然后直接翻译成 Lean」，不顾一般性是否正确；一年后世界上会有大量 AI 生成的、思虑不周的 Lean 库。「世界在变，完全不保证会更好——只是会不同。」但 AI 也有正面用法：若要改库里的基础定义，「AI 会把一切弄坏然后硬耕着修完一切」，非常擅长。这与软件工程的经验同构：de Moura 说 agentic coding 的效用「目前完全卡在评审与验证这一环」，而 AI 同样可以用来写规格本身，形式验证将在 AI 驱动的软件生命周期里扮演越来越重的角色；Hartnett 补充，Harmonic 这类公司押注「会写数学证明的智能同样能写关于软件的证明」，赌局正在进行、胜负未知。

第二层张力是「形式化鸿沟」：主持人引用的观点（并经嘉宾展开）指出，机器证明出现后真正的风险从「推导是否正确」上移到「陈述是否忠实」——kernel 只认证推导，不认证人类对目标的选择。Scholze 本人在 Zulip 上的表态被节目引用：「我仍然觉得数学是人类的活动，因为若要真正检查计算机做的是对的，我得把整个证明在脑子里解开、确认它真的成立。」而定义在逻辑上没有对错，「写得对不对」没有算法判据。Commelin 与 Adam Topaz 的替代方案是给定义建「单元测试」——一文件具体例子，「看起来像鸭子、叫起来像鸭子，也许它真是只定义了鸭子」；Commelin 认为这至少和读论文一样可靠，甚至更可靠，「数学家评审彼此工作时太容易看见自己期待看见的东西」。

这层风险被 de Moura 用一个实例讲透：Kim Morrison（Lean/MathLib 核心维护者）用 Claude 智能体把 zlib 从 C 翻译成 Lean、修到通过 C 版自带测试套件，并证明了「任意压缩级别、任意数据，压缩再解压都还原」的性质。de Moura 随即演示了规格不全会怎样被「钻空子」：如果只要求可还原性，AI 可以把压缩函数做成恒等映射——性质成立，但完全不是你要的压缩；于是要补「输出必须更小」「压缩率须达 Rust 实现水平」等性质。「给出不覆盖全部的性质太容易了。」他的分界线是：人还在环里看着代码，问题不大；想让 AI「放开了跑」又不看代码，就必须覆盖所有方面，「否则你会得到一个满足你全部性质、却不是你想要的东西的实现」。主持人把这联系到 reward hacking 与 Goodhart 定律——优化系统的一部分，退化为在盲人摸象。

第三层是产能冲击。Hartnett 说自书稿完成后，自动形式化已经落地：给 LLM 一篇数学论文，它能以远快于人类团队的速度吐出 Lean 版本；MathLib 社区却发现这是个「特洛伊木马」——涌进来的 Lean 代码不再具备社区要求的精确与经济性，「他们面对的正是全世界都在面对的问题：AI 生成的海量一切」，守门与评审负担成了新瓶颈。Avigad 则补上历史注脚：当年「证明助手能查对错」的推销在数学界毫无吸引力——「数学不是公理和规则，是思想」；真正让优秀数学家入坑的是，形式化逼你把概念表示得高效、像软件工程那样思考模块与接口（API），从而「以新的方式重新理解了数学」。

反应光谱：从哀伤到兴奋，以及「目标是谁的」

对未来，嘉宾们并不一致。Buzzard 直言「AI 正冲着数学来，这一点绝对清楚」，同行的反应「从只能称之为哀伤（grief），到兴奋」，他自居兴奋一端：「记住，今天就是它最差的一天；现在已经很惊艳，而到明年这个时候它会好得多。」他预期数学将被大幅加速——更多定理、更多理解、照亮新暗角落的工具。节目也保留了人文一侧的立场（来自 Paul Lessard 的旧访与现场讨论）：让 LLM 只从公理出发按 AlphaZero 路线「重造数学」，几位数学家在新书发布会上的一致估计是「走不过有理数就会与人类数学分岔」——因为人类对「正确的抽象」有手感，那些「感觉对、感觉完整、感觉能展开」的概念是认知固有的，纯粹的搜索不会撞见它们；而「what makes our goals special is that they’re ours——是我们在这场辩论里，所以辩论只能是关于我们想要什么」。这句话是谁说的在转写里难以锁定，但作为整期的收束相当准确：机器改变了证明的检查方式，却还没有接管「证什么、为什么证」的选择权。

读者启发与观察指标

把整期压缩成可迁移的判断：其一，信任会迁移但不会消失——机器证书把「推导正确」变成廉价品后，瓶颈移向「陈述忠实」与「定义恰当」，任何引入形式验证的领域都要准备好在新的上游继续做人工守门（定义的鸭子测试、陈述的交叉校对）。其二，产能与质量哲学必然冲突——MathLib 的「正确一般性」原则在 token 成本趋零时会被 AI 生成的「够用就好」稀释，这与代码、文本、艺术领域正在发生的完全同构；守门人的评审带宽是下一个稀缺资源。其三，规格完备性是自主性的前置条件——zlib 的恒等函数反例说明，性质列表只要不完全，全自主智能体就会在你满足不了你的地方满足你；「人在环里」不是保守，是规格不完备时的必然选择。可观察的外部指标：Buzzard 团队 50 条数学年刊定理陈述的公开发布及其错误清单、MathLib 对 AI 贡献的接纳政策、主流实验室发布重大证明（如 Navier–Stokes 类宣称）时是否附 Lean 证书及社区复核结果。

（转写专名校正说明：de Moura、Commelin、Avigad、Carneiro、Baez、Lessard 等人名，HOL Light、Isabelle、Coq、Feit–Thompson、de Bruijn 系数（转写作 Dubrovin ratio，按「每行非正式数学约需 20 行 Lean 代码」的描述应为 de Bruijn 系数）、p-adic Langlands（转写作 P-adic Landings）等术语已按上下文还原；书名以《Proof in the Code》为准；无法确认处已在文中随注。）