全文 5,000字 | 阅读约30 分钟
（菲尔兹奖得主陶哲轩 AI数学访谈精彩片段）
过去 30 天，数学界接连被 AI 刷屏：
5 月 14 日，DeepMind 用 AlphaEvolve，这是一款突破传统矩阵运算极限的AI算法，打破了 Strassen 1969 年提出的“矩阵乘法极限”，将一项悬而未解的算法难题推进了 56 年；
6 月 7 日，陶哲轩与 AlphaProof 合作，在闭门研讨会上完成对奥数级难题的 Lean 形式化验证，标志 AI-assisted theorem proving（AI辅助定理证明）正式走向落地；
6 月 12 日，OpenAI 的 o4-mini 在 Berkeley FrontierMath 基准上解出多道顶级新题，标志着AI在“自主探索数学结构”上的首次实质性突破。
这些看似零散的突破，背后却有着一个共同原型—— 2025 年 6 月 15 日,在 Lex Fridman 的 3 小时长访谈中，陶哲轩亲口描绘了“ AI 数学流水线”是如何诞生的：
2200 万个定理判断，被拆解为可验证的代码模块；
AI 插件成为证明的自动补全与验证者；
协作方式从天才式解谜，转为“代码式重构 + 系统式复用”。
AI 在数学上有局限，但可以像人类协作。 我像打游戏一样，把难题拆解，再用 Lean、AI 和众包一一击破。
这不是关于未来的预测，而是已经落地的现实：
18 年未解的难题，在 Lean 协作系统中 30 天内连破 3 道；
人类第一次把“证明”这种最高脑力劳动，转化为可验证、可追踪、可协作的流水线系统；
而这套范式，正逐步向其他知识工作领域扩展：科研、工程、写作、金融、药物设计……
本文通过这三个典型案例和陶哲轩的访谈，分析 AI 协作的新趋势，为你提供构建 AI 协作系统的思路。
这不只是一次数学范式的迁移，它是对未来工作形态的预演。
第一节｜AI 助手不是主角，但已在参与证明
从天才一个人想，到协作把问题拆开干
陶哲轩说：自己越来越像一个'组队通关'的玩家——不是一个人闷头解谜，
而是带着一群人、借助 AI 工具、借助代码平台，把一个难题拆成小块、分配任务、来回验证，直到最后拼成通关图纸。
现在我不再试图一个人从头到尾想清楚一个证明， 而是先画出它的骨架，再不断去补缺口、调转顺序， 最后验证整体能不能跑通。 ——陶哲轩
在他主导的最大项目之一中，他和团队一起处理了 2200 万组代数公式之间的关系，最终把它压缩成一套可以一步步被机器核查的数学结构。
传统上，一个数学证明往往像一篇散文，很多地方靠大家都懂的默契跳过细节。但他和团队用的是一种叫 Lean 的代码语言，每一步推理都必须写清楚，并能被机器逐条检查通过。
这听起来有点像用 Excel 去核对一部长篇小说的句法，但陶哲轩说：我喜欢 Lean 的地方在于，它会像魔鬼一样挑剔地告诉你：你这句逻辑不通。而且它可以帮你记录下你已经试过哪些办法，不用反复走弯路。
他把这整个流程比喻成 “多人远程合作打怪”：
每个人只需要负责一个区域的线索，不用通盘理解；
AI 帮大家补缺逻辑、找错误，甚至推荐下一步的尝试方式；
所有进展都被保存在版本库中，彼此之间可调用、可回滚。
也就是说——AI 没有数学'嗅觉'，会犯微妙错误，但作为智能工具能协助数学工作，在人类监督下提升协作效率。
AI 理解数学有限，但可以当严厉的帮手
过去，证明是靠一个人死磕；现在，它可以被拆成很多子任务，在人+AI+协作平台的帮助下，被一段一段推进、确认、最终合成。
Lean 和 AI 插件已经不只是工具，它们变成了合作者， 帮助我把思路一点点拉清楚、写完整。
这正是他的关键判断之一：
AI 不会发明灵感，但会让每一小步都可追踪、可纠错；
数学不再靠一个天才独挑，而是像开源软件那样，被大家一点点构建起来；
这种协作方式，才是真正让 AI 发挥最大作用的地方。
陶哲轩说自己现在处理难题的方法已经彻底改变：
不是先想一个完整的好办法， 而是先把问题拆散，借助工具一点点试探， 最后再像拼积木一样组合成一个能说得通的答案。
第二节｜从解谜到组装：数学家的新工作法
证明变成了多人线上协作，像做项目一样分任务、拉进度
陶哲轩说，他过去做数学研究时，很像一个人在山洞里苦思冥想。
但现在，他的工作方式更像是 远程团队协作：
“把一个大的目标切成 10 个模块， 每个人各自推进一部分，然后交给 AI 去连接和检查。”
这不是一个比喻，而是他在项目中真实采用的方法。
以他参与的一个重要项目为例，团队用 Lean 语言把一整个证明拆分成了很多步骤节点，每一位协作者负责其中的一段，写清楚推理逻辑、列出所需条件。所有的进展都存放在一个在线的“版本库”中，其他人可以随时查看、补充、或者接着往下推进。
AI 在其中的角色，就像一个永远在线的助手： 当你写不下去时，它会推荐你可能的下一步； 当你逻辑出错时，它立刻给出提示； 当有重复、冗余或可简化的地方，它也会标记。
陶哲轩说： 我们甚至设计了脚本，自动提醒这一段之前已经做过了， 就像写代码时的自动补全、重复检测功能。
过去的数学家靠一个脑子撑起整座楼；现在的数学家更像一个项目经理，组织人力、调用工具、合理安排推进节奏。
AI 负责补空缺，人类负责怎么走
在陶哲轩设计的协作方式中，角色分工变得非常清晰：
人类数学家： 主要负责整体思路设计、提出猜想；
AI ： 提供你可能要的下一步，或提出反例；
Lean： 语言 用来检查整个逻辑链是否通顺、是否缺条件。
他说得非常形象：
“你可以把 Lean 想象成一个非常严苛的编译器， AI 就像一个能自动提示你要用哪个函数的 IDE， 而你是那个站在前线，调度一切的人。”
这个流程听上去像工程，但本质依然是做数学。
唯一的区别是： 你不再靠脑子硬撑，而是有了一套分工明确的协作方法。
这种方法的好处是显而易见的：
有记录：每一步都可以回看、复用、引用；
有反馈：哪里没讲清楚，机器立刻指出来；
有提醒：AI 插件帮你想起你忘了的东西；
有协作：其他人可以在你停下的地方接着往下做。
这让数学研究，第一次从封闭探索，转向公开协同。
就像写代码不再靠一个人闭门造车， 而是靠开源社区逐步构建。
这一节告诉我们：AI 并不是在替代数学家，而是在协助每一步推进。
而更深层的变化是： 数学证明已经不再是表达式，而更像是可编排的流程，
第三节｜不是灵光一现，是协作链在生效
AI 不是解题机器”，是一个“懂格式、能帮忙”的助手
陶哲轩举了一个自己工作中的例子：在 Lean 上写证明时，很多时候他会卡住，不知道下一步该怎么接。但只要调用 AI 插件，它会自动根据上下文，给出几种可能的方式继续写下去。
“它其实不理解我在干什么， 但它能从历史数据中学出很多模式， 并猜出我可能想做哪一步。”
他把这个过程比喻成：AI 就像写作时的自动补全，但不是词语，而是逻辑思路。
比如，当你已经列出一组公式，AI 可以自动判断是否能从这些公式推出目标结论，并在 Lean 中尝试几种常见的推理方法。
如果推理成立，Lean 就会显示验证通过；
如果失败，AI 会建议其他方式，或者指出可能缺了一个条件。
这并不是AI 解题，而是AI 帮你试各种可能性，看哪种能走通。
AI 没有数学直觉，但可以大规模试错 + 学人类经验
在这场访谈中，陶哲轩很坦率地指出：
“AI 没有真正的数学直觉，也没有真正的理解力。 但它的优势在于：可以快速遍历大量选项，并从人类提供的证明中学出套路。”
这就像一个不会下棋的助手，却能记住上万个高手的棋谱。它不一定知道为什么这么下，但知道你在类似局面下，常常会走什么。
他说，AI 学的是模式和套路：
人类过去是凭直觉试错；
现在 AI 帮你补上你没想到但别人用过的套路。
比如，在几何证明中，AI 插件会尝试引入辅助线、坐标变换、角度恒等式等不同方法——它不理解这些方法的“美感”，但能学会什么时候这些办法有效。
陶哲轩说得很形象：AI 是一个没有创造力但不知疲倦的学徒，能够不断尝试、不断提醒、不断协助。
所以，在他看来：
AI 的角色不是提出结论，
而是为人的直觉补上工具箱，
让整个过程从“靠直觉蒙”变成“靠搜索带路”。
这也正是我们需要理解的转变：
AI 变成数学家背后的那套“建议工具 + 尝试引擎”。第四节｜你和 AI 不能合作，只因为说话方式不同
不用同一种语言，人和 AI 合作很快就鸡同鸭讲
陶哲轩在访谈中提到一个非常现实的问题：
AI 可以帮忙，但前提是你能清楚地告诉它你要干什么。
很多时候，人类数学家的表达是模糊的、不完整的。 而 AI——尤其是像 GPT 这样的语言模型——虽然看起来懂，但其实并不能处理含糊其辞。
于是就出现了协作失败的根本原因： 人类说的是“灵感”，AI 理解的是“格式”。 中间只要缺了一个桥梁，就无法真正合作。
这也是陶哲轩为什么极力推动用 Lean 语言写证明的原因之一。
Lean 是一种形式化语言，要求每一步逻辑都清晰明确，写成之后既能被人理解，也能被 AI 检查、扩展、反馈。
他说：我不用 Lean 来取代自然语言，而是让它变成一个协作接口， 人和人之间、人与 AI 之间，都可以通过它来理解彼此的思路。
举个例子：
当你在 Lean 里写出一步推理，AI 插件可以基于它判断（校验）有没有出错，并推荐下一步；
其他合作者也能在这条逻辑链上接着补充，不用重头来过；
整个协作过程像是在使用一个通用翻译器，大家讲的都是同一种格式，才能合力推进。
这其实就像工程领域的 API 接口：只有定义清楚、格式统一，别人才接得上。
数学家第一次需要像工程师一样“写接口”，来组织协作
陶哲轩说，自己现在像在写“别人能看懂并接着用的思路”：
“过去我在黑板上写的东西只有我看得懂， 现在我写的每一个逻辑步骤，都需要别人能接着往下走， 所以我开始在意：这段思路能不能被别人理解。”
这也是他强调数学协作进入工业化阶段的核心变化之一：
不再是发表一篇别人看不懂的论文就完事，
而是要把一个想法，写成所有人都能继续参与的“可共享格式”。
AI 只是加速器，真正促使协作变革的，是这个“语言接口”本身。
这不仅对数学家有启发，对于任何知识工作者也一样：
你的思考方式、表达结构，未来能不能让 AI 看得懂？
你的写作/方案/推理，能不能被别人协同、复用、构建在上面？
你有没有一套“标准表达法”，让你的内容变成别人可合作的起点？
这些问题，其实已经不只是技术问题，而是下一代知识工作者的能力升级标准。
第五节｜知识工作第一次有了“流水线”
18年难题30天就连续攻克了3个，说明了什么？
在陶哲轩的团队项目中，有一个特别的节点：一道 18 年未被攻破的猜想，被他和协作者们用 Lean 拆解重构后，在短短 30 天内就被连续三次不同方式证明成功。
他们不是靠某个人的天才灵光一现，而是靠把问题拆小、组织清楚、逐步验证，最后在多条路线上都得出了成立的结论。
这不是巧合，也不是运气，而是流程变了。
Lean + AI + 协作仓库，把证明过程变成了“可重复执行”的工作流。它不靠灵感，而靠：
步骤明确；
节点共享；
工具自动反馈；
AI 做补充建议与快速试错。
这种做法让一项高门槛的脑力工作，变得更像软件开发：可以版本控制、协作推进、多人共建、结果复用。
过去是天才一个人硬解，现在是人和 AI 一起跑通流程、逐步推进。
这就是陶哲轩所谓的“数学流水线”雏形。
真正被重构的不是数学，而是你每天在做的知识劳动
你可能会问：这跟我有什么关系？我不是数学家。
但陶哲轩的启发远不止数学。
他说：
证明不过是一种特殊的知识生成活动， 但写文章、做规划、设计模型，本质上也是‘用逻辑组织知识’。
而这类工作，都可以被拆成模块、挂上反馈回路、放入可共享的平台中协作完成。
他进一步指出：我们正在进入一个阶段——不是靠一个人‘做完一件事’，而是靠一套流程‘组织所有可用的人+工具’。
比如：你写一个研究报告，以后不是全靠你自己，而是：
开题阶段让 AI 帮你查全已有资料；
拟结构阶段用知识库补全逻辑链；
具体写作时调用 AI 插件按风格补段落；
最后由你审核、微调、提交版本。
这一整套，就是一个可重复使用的知识生成流程。
而它在数学中率成功落地，很快会蔓延到：
咨询文件撰写、商业模型构建；
投资分析、市场策略制定；
甚至 AI 本身的训练与评估。
所以我们必须看清： 不是 AI 替代你思考，而是你要重新组织你的思考方式，让它适配 AI 协作。
就像陶哲轩说的：
未来不仅是个人技术能力的竞争， 更是组织高效协作网络能力的竞争。
这才是知识流水线的核心本质——不是偷懒，而是提效；
不是放弃思考，而是重构组织方式。
第六节｜不是会用 AI，而是会组织 AI
不是会不会用 AI，而是你有没有组织协作的能力
从陶哲轩的工作方式我们可以看出，真正被改变的不是'做证明'这件事，而是思考、协作、表达的基本方式。
我不会说 AI 是在‘解数学题’， 但它改变了我‘做数学的方式’。 ——陶哲轩
这句话背后是一个更大的提醒：
AI 不会替你解决核心问题，但它能组织解决问题的流程；
它不会直接给出正确答案，但它能提示、连接、提醒、验证。
这对每一个知识工作者都意味着新技能标准：
✅ 能不能把问题分解，让 AI 帮你尝试每一段？
✅ 能不能把自己的工作分阶段描述清楚，交给不同工具协助？
✅ 能不能把自己用过的逻辑/结论模块化，方便团队和未来自己复用？
这就是协作能力，不是精通某个 AI，而是你有能力构建一整套支持 AI 协作的工作流。
你的知识劳动，从'做完就完'变成'别人能接着用'
陶哲轩强调，他做 Lean 项目的时候，不再追求一次解出，而是让每一步都能复用、共享。
这意味着什么？
你写的一段分析报告、一个解决方案、一个表述逻辑，如果组织得好，将来可以反复利用、持续演化，甚至由他人接力扩展。
不再是我做完就结束，而是“我构建一块积木”；
不再是重复劳动，而是“模块积累”；
不再是每次推倒重来，而是“共享+自动建议”。
这个范式变化已经在数学中先行爆发，在你还没注意的时候，已经悄悄扩散到知识密集型的每一个行业。
未来不只是谁知识多，更是看谁先把知识流程做成工具化。 ——陶哲轩
AI时代，知识工作者要关注的重点变了：
不要再只关注 AI 工具怎么用，而是从现在开始：
训练自己用 “可协作的方式” 组织工作内容；
积累能被 AI 理解的素材、流程和表达方式；
这不只是技能变迁，是职业生存方式的整体重塑。
结语｜不是理解 AI 数学，而是提前适应 AI 工作方式
陶哲轩没有预测未来，他只是提前活在了未来。
因为他已经把最难的数学证明流程，拆解成了一个由人、AI 和格式语言协作完成的知识生产链。
这不是什么高门槛的事，人人都能做：
不需要你一开始就有答案，但你要会把大问题切成小问题；
不需要你亲自写完所有内容，但你要知道怎么带团队干活；
不需要你懂高深理论，但你要学会借助各种 AI 工具。
过去，知识是一次性输出； 现在，知识是一套“可被协作、可被调用”的资产。
这才是 AI 真正改变的，不是人类的能力，而是工作的方式。
对每个人来说，现在就是最好的起点：
从今天开始，学会构建自己的AI协作系统。
本文由AI深度研究院出品，内容整理自陶哲轩与 Lex Fridman 的最新对话。未经授权，不得转载。
星标公众号， 点这里 1. 点击右上角 2. 点击"设为星标" ← AI深度研究员 ⋮ ← 设为星标
https://www.youtube.com/watch?v=HUkBz-cdB-k&t=18s&ab_channel=LexFridman
https://deepmind.google/discover/blog/alphaevolve-a-gemini-powered-coding-agent-for-designing-advanced-algorithms
https://www.reddit.com/r/singularity/comments/1knem3r/i_dont_think_people_realize_just_how_insane_the
https://spectrum.ieee.org/deepmind-alphaevolve
https://finance.sina.com.cn/tech/csj/2025-06-07/doc-inezfuhz9534450.shtml
https://www.ft.com/content/564403fa-134c-4385-9e57-4cfc53880508
来源：官方媒体/网络新闻，
排版：Atlas
编辑：深思
主编：图灵
热门跟贴