transcript
show notes
今年 1 月 13 号，在 arxiv 出现了一篇论文（2601.07222），它证明了代数几何里的一个新定理，特别的是，这篇文章中的一个重要证明是由谷歌的 Gemini 模型生成的。文章作者之一，美国数学学会主席 Ravi Vakil 教授评价道，Gemini 的证明严格、正确，优雅，并不是已有文献的重组。教授表示，如果这个证明是他本人做出来的，他也会因此觉得自豪。
类似的新闻我们最近听到得越来越多，就比如说，菲尔兹奖得主陶哲轩是 AI 数学的忠实用户和倡导者，自己也参与了用 AI 加上形式化验证来解决数学问题的工作。
本期嘉宾 Alex Gu 就是陶哲轩在 AI 数学上的合作者之一，他所在的 8 人创业公司 Math, Inc 邀请了陶与他们合作，共同开发他们的 AI 形式化数学 Agent 高斯，并在 1月 16 号刚刚完成了对超椭圆曲线的黎曼猜想及其证明的形式化。本期 AI 实话实说，我们想和他深入聊聊：AI 做数学，到底能代替数学家吗？
Alex 是 MIT PhD on leave，之前的主要研究兴趣是 AI for code 和 AI for math。大家耳熟能详的 LiveCodeBench 评测就是他的作品。
相关术语：
formal math - 形式化数学，在我们的语境下指用 lean 等计算机语言书写，利用编译器检验正确性的数学
informal math - 非形式化数学，在我们的语境下指人类目前更常用的由人类审稿人来检验正确性的数学
快速跳转：
0:00:55 引入
0:02:27 嘉宾经历介绍
0:11:24 什么是形式化数学？
0:15:40 为什么大家用 lean 来做形式化数学？
0:17:00 形式化证明的例子
0:20:43 在 AI 出现以前，大家做形式化数学的动机是？
0:22:59 AI 出现以前形式化数学为什么没有大规模使用？
0:26:15 形式化费马大定理，需要数学家还是 AI 人？
0:28:39 为什么大家应该用 AI 做形式化数学，而不是 informal math？
0:33:38 形式化和非形式化的数学对数学家有什么用？
0:34:56 什么叫自动形式化？为什么它对于 AI 数学重要？
0:40:00 到底哪些人在做 AI for formal math？
0:42:37 不同的动机做 AI 数学，会产生什么样的不同行为？
0:48:02 formal math 天生不适合人类数学家阅读吗？
0:51:10 创业公司为什么要做 AI for math？
0:53:58 AI math 创业公司有哪些？讲的是什么故事？
1:01:59 AI 数学将来可以应用到软件的形式化验证？
1:07:09 AI 数学还有哪些可能的应用场景？
1:13:47 数学家群体怎么看待 AI 数学？为什么有些数学家不喜欢 AI 数学？
1:18:16 “手工”数学家和拒绝工业化的手工铁锅匠人有区别吗？
1:20:15 数学家未来会拥抱 AI 吗？
1:22:12 Math Inc 如何团队合作？
1:24:57 Math Inc 如何和数学家合作？
1:26:40 陶哲轩如何和 Math Inc 合作
1:29:34 为什么陶哲轩喜欢 AI 数学？
1:33:18 你们会如何改变数学博士的就业市场？
1:36:18 对于现在要开始学数学的人有什么建议？
1:38:21 AI 不擅长提出新猜想和新问题吗？
1:46:14 为什么加入创业公司，而不是大厂？
嘉宾主页：
相关论文：
Formal Mathematical Reasoning: A New Frontier in AI
感谢 Peiyang Song 对本期节目的贡献。
在小宇宙查看该单集文稿