2026 年 9 月 11 日，哈佛大学数学科学与应用中心（CMSA）「2026 机器学习的几何」（The Geometry of Machine Learning 2026）研讨会进入最后一天。斯坦福大学数学系 Szegő 助理教授 Jared Duker Lichtman 做了一场约 44 分钟的演讲，题目是《形式化与数学的未来》（Formalization and the future of mathematics）。演讲结尾只有一句话：先测绘疆域，提供坚实的地基，然后出发去探索数学的前沿。
Lichtman 为 MAP 计划选用的配图，对应他把 MAP 比作「数学界的人类基因组计划」——人类基因组计划测定了人的全部遗传信息，MAP 则要把人类全部已知数学知识测定为机器可检验的形式化代码。图片来源：Jared Duker Lichtman《The MAP: Mathematics Autoformalization Project》
Lichtman 是数论学家，博士师从牛津大学的 James Maynard，学生时代就因证明 Erdős 本原集猜想而成名，近两年又深度参与了 Math Inc 公司自动形式化智能体 Gauss 的工作。这样一位做素数分布出身的数学家，站在讲台上宣布了一件听起来离谱的事：人类已经具备在一年之内把全部已知数学翻译成形式化代码的条件。他把这件事比作数学界的人类基因组计划，或者这个时代的 AlphaFold。
这场演讲的核心论据是一条增长曲线、一个 1300 万行代码的证明，和一个叫做 MAP 的计划。
本文目录
- 一、费马大定理的 1300 万行 Lean 代码
- 二、五个数量级的增长曲线
- 三、MAP：给全部已知数学测绘一张形式化地图
- 四、从验证到发现：压缩与展开
- 五、演讲者的来路
- 六、结语
一、费马大定理的 1300 万行 Lean 代码
演讲的叙事起点是九天前的一次震动。2026 年 9 月 4 日，Anthropic 宣布 Claude 完成了费马大定理（Fermat's Last Theorem）的端到端形式化证明：一个内部研究模型在 11 天里基本自主工作，写出超过 1300 万行 Lean 代码，沿途证明了约 3 万个中间定理，其中 29500 个进入最终证明，消耗约 60 亿输出 token。
费马大定理由费马在 1637 年提出，1995 年由 Andrew Wiles 和 Richard Taylor 证明。就在不久前，帝国理工学院的 Kevin Buzzard 刚启动了一个形式化费马大定理的项目，拿到了 90 万英镑资助，计划用 5 年完成。这在圈内长期被视为天方夜谭式的工程，因为即便 5 年做完，也只触及表面——Wiles 的证明还依赖 20 世纪数学文献里的大量前置结果。Claude 用 11 天连前置文献一起形式化了，这就是这件事的冲击力所在。
这次成功的技术路径同样值得记录。早期尝试失败后，项目切换到 Prove2Me——一个由 Anthropic 研究员 Tianyi Peng 和哥伦比亚大学合作者设计的开放式协作形式化平台。
Prove2Me 维护一张待证定理的有向无环图（DAG），几十个 Claude 智能体围绕这张共享图并行工作，一个智能体证完的定理立刻成为其他智能体可用的依赖；它还把定理陈述和证明拆到不同文件里以加速编译，并为每条定理维护自然语言描述以便检索复用。最终产出的证明通过了三重检验：Lean 标准内核、用 Rust 独立实现的 nanoda 内核，以及 Mathlib 社区的 comparator 工具（专门核对形式化陈述是否就是定理本身而非弱化版本）。
整个证明只使用 Lean 的三条标准公理。形式化沿用的数学路线是 Darmon、Diamond 和 Taylor 对 Wiles 证明的简化版讲义，人类的数学输入只有 Tianyi Peng 偶尔给出的高层指示。Buzzard 审阅后的评价是：自动形式化的产物已经足够可靠，可以在上面继续建造。
Prove2Me 提出的协作机制与专用 harness，让众多智能体能在彼此工作的基础上继续构建，把数学形式化变成任何人带一个智能体就能参与的规模化众包工程。
对 Buzzard 个人而言，这件事解锁了一个更具体的愿望：形式化朗兰兹纲领相关的文献。他担心那里面藏着微妙的错误，而机器检验能把这些错误找出来。
二、五个数量级的增长曲线
Lichtman 强调，费马大定理算不上孤立事件，它只是落在一条增长序列的最新一点上。他按时间列出了自动形式化（autoformalization，指 AI 把自然语言数学自动翻译成 Lean 等形式化代码）的规模纪录：
- 2024 年 7 月，DeepMind 拿到 IMO 银牌还是领域巅峰时，纪录大约是 400 行代码；
- 2025 年 6 月，de Bruijn 的 ABC 定理形式化，纪录跳到 3500 行；
- 2025 年 9 月，素数定理强形式的人工辅助自动形式化突破 2.5 万行，完成了陶哲轩和 Alex Kontorovich 在 2024 年设下的挑战（这正是 Lichtman 本人参与、由 Math Inc 的 Gauss 智能体完成的工作）；
- 2026 年 3 月，Maryna Viazovska 获菲尔兹奖的球体堆积（sphere packing）工作被自动形式化，总计 20 万行；
- 2026 年 6 月，OpenAI 自动形式化 Erdős 单位距离猜想的相关工作，越过 100 万行；
- 2026 年 9 月，Claude 的费马大定理证明达到 1300 万行。
两年之内，五个数量级。Lichtman 特意指出，单看费马大定理的体量已经够惊人，而把这条曲线画在对数坐标上，趋势会看得更清楚：它几乎是一条平滑的指数直线。
线性坐标下，前五个里程碑因数值偏小紧贴横轴几乎无法分辨，费马大定理的 1300 万行在 2026 年 9 月垂直拉起，最后一跳显得像突变。图片来源：Jared Duker Lichtman《The MAP: Mathematics Autoformalization Project》
换成 10 的幂次后，六个里程碑排成一条接近直线的平滑轨迹，说明费马大定理并非失控异常值，而是指数趋势的按时到达。顺着这条直线外推，覆盖全部数学教科书和研究文献大约需要数百亿行代码。图片来源：Jared Duker Lichtman《The MAP: Mathematics Autoformalization Project》
三、MAP：给全部已知数学测绘一张形式化地图
顺着这条曲线，Lichtman 提出了 MAP（Mathematics Autoformalization Project，数学自动形式化计划）：创建一个覆盖人类全部已知数学的综合形式化数据库。
他给的类比是 AlphaFold。AlphaFold 把人类已知的 2 亿个蛋白质结构全部制表，MAP 要在数学里做同样的事。数学知识是累积式的——研究生课程的代数、分析、几何、拓扑、应用数学建立在本科内容之上，教科书建立在课程之上，研究文献建立在教科书之上——所以测绘必须按地形一层层推进，而最终成果会是人类数学已知疆域的第一张完整地图。
总量估算按 Claude 当前的效率计算：全部数学语料大约在 100 亿行代码量级，这还不考虑未来的效率提升。Lichtman 的判断是，只要学术界、前沿实验室、慈善机构和政府之间有充分的协调与资金投入，这件事在接下来一年内就能做到。他在文末感谢了 DARPA expMath 项目的负责人 Patrick Shafto，以及为 MAP 出谋划策的 Eric Weinstein。
MAP 的价值首先是验证。其他科学领域饱受可复现性危机困扰，而形式化过程能直接标出文献里的错误——历史上这类错误偶尔动摇过整个研究方向，在近期的 AI 数学成果里已经能看到这类早期案例。但 Lichtman 把话说得更远：MAP 同时是下一代研究的基础设施，是未来数学的地基。
四、从验证到发现：压缩与展开
对「AI 数学成果有没有原创性」这个问题，Lichtman 给出了一个冷静的观察。头条新闻里那些 AI 生成的数学成果固然令人印象深刻，但它们的证明本身缺乏真正的原创性——本质上都是已知方法的巧妙组合。
目前很多关于 AI 数学的评论默认这种状态会永远持续下去，认为 AI 永远不会有新颖的洞见。他不接受这个默认，理由就在 MAP 本身：完全显式的形式化代码，能为下一代模型提供精确的训练场。全部已知数学被写成机器可读的显式代码之后，模型第一次有了一份没有省略、没有含糊、每一步都可检验的训练材料。
这也呼应了前文里的另一个判断：在这个新世界里，压缩（compression）与展开（expansion）这两条原则会成为根本。这次研讨会上，Logical Intelligence 的 Mike Mulligan 在开幕演讲中正好论证过同一个主题：人类数学家发现和珍视的「人类数学」，只占全部有效演绎的极小一部分，它的标志恰恰是可压缩性——层层嵌套的定义和定理让知识以多项式而非指数的方式增长，压缩本身可以作为衡量数学趣味、给智能体指路的标尺。Lichtman 的 MAP 提供原料，压缩提供方向感，展开则是在地基之上向未知疆域的探索。
演讲的结尾是一句话：先测绘疆域，提供坚实的地基，然后出发去探索数学的前沿。
Lichtman 为 MAP 章节选配的古地图。中世纪航海图上的空白处标着未知海域，今天的数学文献里同样有未被检验、未被连接的空白。把全部已知数学形式化，就是把这张地图的已知部分完整绘制出来。图片来源：Jared Duker Lichtman《The MAP: Mathematics Autoformalization Project》
五、演讲者的来路
Lichtman 在演讲里用了一段篇幅交代自己为什么会站在这个位置上。他的数学生涯从数论开始，2019 年到牛津跟随 James Maynard 读博士，动机是素数的奥秘。同在 2019 年，Kevin Buzzard 在牛津的研讨会上讲了一门叫 Lean 的新编程语言。Lichtman 的原话是：那场演讲重新接上了他的神经。Buzzard 解释了自然语言数学怎样翻译成 Lean，于是证明的正确性变成了一段程序的编译是否通过。Buzzard 本人则是在 2017 年听了 Tom Hales 讲开普勒猜想历史性的形式化之后「上了瘾」——开普勒猜想也是个几百年的老问题，证明复杂到人类审稿人无法确定地核查，经过十多年的努力最终被形式化。
Buzzard 把这件事叫做「数学的数字化」。Lichtman 当场被说服，与此同时他知道另一条平行的革命正在发生：ImageNet、AlphaZero、Transformer，再到聊天机器人和这一年的智能体，AI 革命一路走高。
过去几年他自己的工作一直在数论里，只是远远地观察 AI 和形式化的进展——手工形式化是一门专门的手艺，连专家翻译一小段自然语言数学都要费很大力气。而这一年，他发现自己站到了数学史一个独特时刻的前线：AI 革命和形式化革命汇合成了自动形式化。
他还讲了一个细节。当年他远远观察时，身边多数同事对 AI 的进展速度和它会给数学带来的影响都不以为然。他没有争论，但一直觉得这种轻视令人困惑。过去一年的进展验证了他的判断，也正是今年他意识到自己应该出来说话——在数学正在经历转型、外界普遍感到困惑和混乱的时刻，这样的声音比以往任何时候都更需要。
Jared Duker Lichtman，1996 年生，斯坦福大学数学系 Szegő 助理教授、斯坦福 HAI 教职成员，曾用初等方法完全解决 Erdős 本原集猜想。
六、结语
这场 44 分钟演讲的内容想表达三层意思。
- 第一层是事实：自动形式化的规模两年涨了五个数量级，费马大定理的 1300 万行机器可检验证明已经公开在 GitHub 上，只依赖三条公理。
- 第二层是计划：MAP 要在一年内把全部已知数学——约 100 亿行代码——变成形式化数据库，做数学界的人类基因组计划。
- 第三层是判断：验证只是开始，形式化代码将成为下一代模型的训练场，压缩与展开会成为新世界的根本原则。
这里可能需要有一个清醒的认识：一年完成全部数学的形式化，是 Lichtman 作为当事研究者提出的雄心，目前既没有落实的资金承诺，也没有既定的时间表；Anthropic 官方也承认费马大定理的证明代码比实际需要长得多，形式不适合直接进 Mathlib，前置定理只在需要的特殊情形下证明，下一个项目无法直接复用。
从 1300 万行到 100 亿行，要的不只是模型能力，还有今天还不存在的基础设施。但反过来，五个数量级的曲线摆在那里——两年前说「11 天形式化费马大定理」的人，同样会被当成疯子。这张地图最终画成什么样，值得盯着看。
发表于 9 小时前
|
查看: 5|
回复: 0
