陶哲轩办公室有 6 块黑板，他说绝不放弃。但他刚带 50 个人用 AI 和代码解决了 2200 万道数学题。
这位 Fields 奖得主在 2026 年 2 月的 SAIR 基金会“AI for Science: Kickoff 2026”活动上，用 17 分钟讲了一件事：数学这个几百年没变过工作方式的领域，正在被新技术撬动。 而撬动它的关键，不是 AI 本身，而是一个大多数人没听说过的东西。
原始视频链接：https://www.youtube.com/watch?v=mS9Lr43cIB4
要点速览：
注： SAIR（Foundation for Science and AI Research）是陶哲轩联合创办的非营利基金会，致力于用 AI 加速科学发现。本次活动由 SAIR 与 UCLA 的 IPAM 联合举办。
陶哲轩在演讲开头展示了一本 1826 年 Cauchy 写的数学教科书。
除了是用法语写的、不是用现代排版工具排的，跟我们今天给研究生用的几乎一模一样。 （“Other than it's in French rather than English and it's not typeset using a modern computer language... it's completely usable today.”）
这种 200 年的连续性是数学的力量。勾股定理是两千多年前的成果，陶哲轩说他自己的研究中经常使用。但代价是：数学家极度保守，几乎是最不愿拥抱变化的学术群体。
他举了一个有趣的细节：数学家恐怕是唯一还守着黑板和粉笔的学术学科了。其他领域早就换成了 PPT 和白板。摄影师 Jessica Wynne 甚至专门拍了一本数学家黑板的摄影集《Do Not Erase》（别擦掉），出版后成了一本艺术画册。
注：《Do Not Erase》由 Princeton University Press 于 2021 年出版，收录了 100 多位数学家的黑板照片，陶哲轩的黑板也被拍进去了。
而陶哲轩自己呢？
我办公室有 6 块黑板。我爱它们。我不会放弃的。 （“I have six blackboards in my own office. I love them. I will not give them up.”）
陶哲轩展示了一张各学科论文平均作者数的变化图。其他科学领域的协作人数在爆炸式增长，数学呢？从 1.5 人缓慢爬到了 2.5 人。
他自嘲说，不是因为数学家反社会，或者说“不只是因为反社会”。真正的原因有三个：
第一，门槛太高。 你通常得有数学博士学位才能理解自己在做什么问题。
第二，正确性要求极端。 如果你众包一个证明，100 份贡献里有 1 份是错的，整个证明就废了。
如果你尝试众包一个证明，100 个贡献中有一个是错误的，就毁掉了整个证明。 （“If you try to crowdsource a proof and there's 100 contributions and one of them is incorrect, you destroy the whole proof.”）
第三，工作流没法扩展。 数学家的核心工作方式是两三个人站在黑板前讨论，这没法 scale 到 100 人在线协作。
但其他科学已经在这样做了，而且蓬勃发展。
数学是不是错过了什么？
陶哲轩说，变化正在发生。他用了一个精辟的框架来描述：过去的数学研究是“案例研究”模式，一次挑一个问题，花几个月产出一篇论文，再去做下一个。现在开始出现“大规模调查”模式，同时处理数百甚至数千个问题。也许不能全部解决，但可以报告这些问题群体的有趣统计规律。
参与者也在拓宽。其他学科的“公民科学”已经很成熟了，数学才刚开始出现“公民数学”。
注： 公民科学（citizen science）指非专业科学家参与科研项目，比如天文爱好者帮助分类星系图像。数学领域此前很少有这种模式。
至于 AI？陶哲轩的措辞很有意思：
我们发现了很多使用机器学习和 AI 的错误方式，但才刚开始从这些工具中获得一些有用的价值。 （“We've discovered lots of incorrect ways to use machine learning and AI, but we're just beginning to get some useful mileage out of these tools.”）
而让这一切成为可能的，有一个”秘密武器”。
这个秘密武器不是 AI，而是形式验证（formal verification）。
简单说，形式验证是一种特殊的计算机语言，能接收一段数学论证，自动判断它对不对。陶哲轩说，这一个能力就“过滤掉了大量垃圾”，移除了此前阻碍新工作流的最大障碍。
为什么这么重要？因为它直接解决了前面提到的“100 份贡献里 1 份错误就毁掉整个证明”的问题。有了自动检查，你不再需要信任每个贡献者，只需要信任验证系统。
注： 目前数学形式化领域最活跃的工具是 Lean，由微软研究院开发的证明助手语言。它不仅能验证证明对不对，还能像 IDE 一样在写证明过程中实时提示哪一步出了问题。
陶哲轩花了最多篇幅讲这个案例：Equational Theories Project（等式理论项目）。
他在 UCLA 发起了这个项目，共 50 位协作者参与。但这些人大多数他从未见过面，是通过项目才认识的；大多数也不是专业数学家，而是计算机科学家、研究生、本科生，他说甚至可能有高中生。
项目的任务是：程序化生成了 2200 万道代数蕴含关系问题。比如，如果一个运算满足交换律（a*b = b*a），能推出它也满足结合律（(a*b)*c = a*(b*c)）吗？答案是不能。但这样的问题有 2200 万个。
注： 准确地说，是 4694 个 magma（只有一个二元运算的代数结构）等式定律之间的两两蕴含关系，共 22,028,942 对。项目于 2024 年 9 月 25 日在 GitHub 上启动，最终论文于 2025 年 12 月上传 arXiv。
单独来看，每道题可能一个代数方向的研究生花一小时就能解。但 2200 万道？
我可没有 2200 万个研究生。 （“I don't have 22 million grad students.”）
你可以说“那就众包吧”，但谁来批改 2200 万道题？以前同类型的研究最多处理过 20 个问题。
他们三个月就做完了。每一道都有证明或反证。
怎么做到的？所有证明存在 GitHub 上，必须用 Lean 语言形式化，这样就能自动验证正确性。协作讨论在 Zulip（一个开源的类 Slack 平台）上进行。有人写出人类可读的证明，有人把它翻译成 Lean 代码；有人写程序批量攻克问题，一次处理 10 万道；有人则把计算机证明转化回人类证明。大量来回迭代，虽然是即兴摸索出来的，但效果极好。
陶哲轩总结了几个关键因素。
第一是模块化。 2200 万个问题天然地拆分成子任务，每个人可以认领一批来做。有人专写人类证明，有人专做 Lean 翻译，不需要理解项目全貌就能贡献。他类比说，”就像现代软件开发项目”。
第二是有一个明确的指标。 在项目第 16 天，2200 万个蕴含关系中只剩 888 个未解决。这个数字就是所有人的目标，把它往下推。有些想法一次能消掉一大批，有些没那么成功。但不需要全局协调，每个人都在自发地把数字往下推。陶哲轩说，参与者的自发行动“看着真的很有趣”。
第三，也是最关键的：形式验证打破了信任壁垒。
以前数学协作的模式是：要么逐行检查别人的工作，要么靠声誉信任对方。但这个项目收到了大量来自陌生人的贡献，有些人从未在数学界露过面。这没关系，所有提交都必须通过 Lean 的自动验证。匿名贡献？可以。不受信任的贡献？也可以。
而且形式验证让讨论变得极其精确。比如有人提交了一个九步证明，前八步都通过了，第九步 Lean 报错。这时候你可以就那一个微小的步骤跟作者讨论。以前没有共同的精确语言，很难定位到底卡在哪一步；现在可以在“原子级别”上进行技术对话。
整个项目中，虽然也用了自动化定理证明器之类的 AI 工具，但陶哲轩坦言：
实际上起作用的是更平凡的技术，就是 GitHub 和 Zulip 这些基本的协作平台，它们简直太有用了。 （“Actually it was the more mundane technologies, things just like GitHub and this discussion group at Zulip. Basic collaboration platforms were just incredibly useful and essential.”）
注： Zulip 是一个开源的群组讨论平台，类似 Slack 但有独特的”话题线程”功能，特别适合技术讨论。Lean 数学社区的主要交流平台就是 Zulip。
演讲进入下半段，陶哲轩转向 AI 和大语言模型。
LLM 越来越强大了，能解数学奥赛题，有时能回答很深的数学问题。但它们会犯错误，而且经常是非常基础的错误。陶哲轩展示了一个例子：某 LLM 被问 7×4+8×8 等于多少，算错了。被指出后道歉，然后给出了正确答案。
每个数学家都试过用 LLM。结论呢？
每个数学家最终都发现，不可靠性是一个太大的问题。 （“Every mathematician has tried using these and has eventually found that the unreliability is too great of an issue.”）
但如果把不可靠的 LLM 输出和一个验证器结合起来呢？让 LLM 生成数学输出，验证器检查是否正确；正确就保留，不正确就把错误信息反馈给 LLM 让它纠正。这个“生成→检验→反馈→纠正”的循环，有时候能跑通。
陶哲轩正在跟 Google DeepMind 合作他们最新的工具 AlphaEvolve。这个工具不只是 LLM，底层还有遗传算法。
注： AlphaEvolve 是 Google DeepMind 开发的”进化式编程智能体”，结合 LLM（Gemini）的代码生成能力和进化算法，通过不断提出、测试、优化代码方案来解决数学和科学问题。2025 年 5 月公开宣布，同年 11 月陶哲轩等人在 arXiv 发表了使用 AlphaEvolve 攻克 67 个数学问题的论文。
他举了一个例子：如果你有 11 个正六边形，能装进去的最小正六边形多大？以前有人类找到的最优记录，AlphaEvolve 通过让 LLM 不断尝试、获取反馈、进化代码，打破了这些记录。
但这些只是测试案例。堆叠问题本质上是有限维优化，只是数学家关心的问题的一个很小的子类。陶哲轩透露，他们在无穷维优化问题上也有了新进展，但”很遗憾，暂时还不能说更多。请关注，几周后我们会发论文。”
演讲收尾，陶哲轩总结了 AI 对数学的影响。
已经在发挥作用的场景：
但要获得更高级的应用，必须依赖严格的验证。AI 单独辅助个体数学家有一定帮助，但和更广泛的协作体系结合时效果最大，它能填补协作中缺失的环节。
我们只能在信任 AI 输出的范围内使用它，或者至少能检查它。超出这个范围就太冒险了。 （“We can only use the AI as far as you can trust its outputs, or at least check them. Any further and it's just too risky.”）
然后他提出了一个和常见想象不同的观点。大家最容易想到的 AI 用途，是用 AI 替代数学家做他们最擅长的事，用创造性的新技术攻克难题。但有一个“正交”的用途，至少在中期内会更有生产力。
数学中存在一条巨大的“中等难度问题长尾”，就像那 2200 万道代数题。人类没有人力一个个去做，但可以让 AI 先跑一遍，把简单的都解决掉，然后把真正难的上报给人类专家。
AI 不应该跟人类已经在做的工作竞争，而应该把蛋糕做大，创造出更多任务，让更多目标在经济上变得可行。 （“AI should be used to not compete with the pie of work that humans already do, but to enlarge the pie and create more tasks — make more objectives economically feasible.”）
他最后补充：这些应用都非常依赖具体场景，不是即插即用的。得知道什么时候该用、怎么用。
此内容由惯性聚合(RSS阅读器)自动聚合整理，仅供阅读参考。 原文来自 — 版权归原作者所有。