陶哲轩用Claude Code解题，为何两度因token不足失败？
近日，菲尔兹奖得主、加州大学洛杉矶分校（UCLA）数学系教授陶哲轩（Terence Tao）在 YouTube 发布了一段时长约 26 分钟的实操视频，详细演示了如何利用 Anthropic 推出的 Claude Code 代理工具，在 Lean 定理证明器中完成一项数学证明的形式化全过程。
（来源：Youtube）
陶哲轩在视频开始就明确了任务目标：将集合论中的“单例定律”（Singleton Law）从非形式化的自然语言描述，转化为 Lean 系统能够编译和严格验证的代码。简而言之，该定律论证了对于任意集合 A 和元素 x，单例集合 {x}属于 A 的条件等价于某些特定的子集属性。
尽管这在数学概念上这属于较为基础的引理，但要在类型论严苛的 Lean 系统中完成形式化，却伴随着大量琐碎且对语法要求极高的代码编写工作。
这并非陶哲轩首次处理这一任务。大约九个月前，他曾在其主导的“方程理论”（Equation Theories）项目中，已经利用当时的主流工具（如 GitHub Copilot）手动完成了该证明。
（来源：Youtube）
这次引入 Claude Code 重做此题，陶哲轩是想直观对比新一代“代理式编码工具”与上一代代码补全工具之间的代际差异。
与 GitHub Copilot 早期仅能基于光标位置提供几行代码自动补全不同，Claude Code 是一个运行在终端的代理系统，能够理解复杂的自然语言指令，自主读取文件目录，规划步骤，并自动执行代码编辑和修改。在陶哲轩看来，这种能力的跃升或许让 AI 有望真正接管数学研究中被称为“繁文缛节”的重复性劳作。
大佬用 AI 也会翻车
有趣的是，视频中所展示的流畅流程并非一蹴而就。陶哲轩在录制中坦言，这是他第三次尝试用 Claude Code 完成该任务。在此之前，他因为不同原因已经“翻车”了两次。
在第一次尝试中，陶哲轩直接给出了一个宏观指令，要求 Claude“完成整个证明”。结果，AI 在连续运行了 45 分钟后，消耗了海量 Token 并导致电脑崩溃，最终未能产出任何有效结果。
有网友直接在评论区@Anthropic：“给陶哲轩开个无限 Token 权限吧，说不定数学 2.0 时代能提前到来！”这话听着像玩笑，却也戳中了当前 AI 工具的一个现实痛点：真干起精细活来，Token 消耗的速度是真快。
（来源：Youtube）
第二次尝试时，他改变了策略，要求 AI 按引理（Lemma 1, 2, 3）分步执行，这次耗时 25 分钟成功完成，但因录屏软件故障未能保存。
吸取了第一次的教训，在第三次（即本次发布的视频）实操中，陶哲轩采用了高度结构化的“脚手架”（Scaffolding）策略。他在文件顶部撰写了一份极其详尽的“配方”（Recipe），将任务拆解为初始定义、大纲搭建以及三个子引理的逐步证明，以此来约束 AI 的行动发散空间。
1. 搭建骨架（Skeletonization）
流程初期，陶哲轩指令 Claude Code 先不要急于推导，而是用 Lean 系统中的占位符“sorry”搭建起整个证明的宏观框架。这一步进行得异常顺利，AI 准确识别了非形式化证明中的逻辑断点，并将其转化为 Lean 代码结构。陶哲轩指出，让 AI 先写出带有“sorry”的骨架，随后再逐一填补，是目前最高效的人机协作模式。
2. 陷入泥潭与人工干预
然而，在具体填补 Lemma 1 的证明细节时，Claude Code 的短板开始显现。由于 Lean 的底层逻辑要求高度严谨，AI 在面对非形式化语言中的等式代换时，表现出“过度思考”的倾向。它试图频繁展开底层的数学定义，而不是机械地按照人类给出的步骤进行推演。
在视频中，AI 在后台进行了大量的回溯和自我试错，消耗了大量计算资源，推导过程变得异常冗长。在这个过程中，陶哲轩的工作站甚至意外宕机了一次。系统恢复后，面对 AI 将简单步骤复杂化的窘境，陶哲轩果断选择人工介入。他直接接管了键盘，迅速输入了一个基于 congr（同余/等式替换）指令的策略，瞬间突破了僵局。
他客观评价道：“过度依赖工具可能会让你失去对证明的直觉。当 AI 陷入死胡同时，人类直接上手往往比等待它纠错要快得多。”
3. 演化出“并行工作流”
随着进程推进到 Lemma 2 和 Lemma 3，陶哲轩展示了令人眼前一亮的工作流创新。当他确认 AI 已经掌握了骨架搭建的技巧后，他不再单纯扮演“监督者”，而是开始与 AI“双线操作”。当 Claude Code 在后台自主分析并试图填补 Lemma 3 的底层逻辑时，陶哲轩则在代码的前段手动补全 Lemma 2 中相对直观的"sorry"部分。
这种人机并行作业的模式，最后将总耗时压缩到了约半小时以内，并且最终代码毫无报错地通过了 Lean 编译器的严格审查。陶哲轩总结称，将任务切分，人类处理一目了然的逻辑，而将需要堆砌代码的繁重任务交由代理，是现阶段最具可行性的实践。
AI 从“平庸助教”到“初级合作者”
若将此次视频置于陶哲轩近年来对 AI 的系列实验史中审视，我们能清晰地看到一条技术跃迁的轨迹。
早在此轮生成式 AI 爆发之初，陶哲轩就曾积极测试各类聊天机器人，并将其比作“平庸但不完全无能的研究生”。彼时的 AI 在处理如微积分中的 epsilon-delta 极限证明时，极易出现幻觉，频繁混淆变量域或遗漏边界条件，更多是作为一种新奇的玩具存在。
到了 2025 年，随着大模型基础能力的提升，陶哲轩曾公开测试 GPT-5 级别模型在复杂学术文献检索上的表现。在那次测试中，AI 能够快速在海量未完全结构化的论文库中挖掘出特定的定理渊源，为他节省了数周的案头检索时间。然而，当时 AI 扮演的仍是“高级图书管理员”的辅助角色，而非直接介入证明的生成。
而进入 2026 年初，形势发生了质的变化。以 ChatGPT 为代表的大模型在著名的 Erdős 开放猜想库中发力，试图“独立”解决这些涵盖数论与组合学数百个未解之谜的问题。陶哲轩的 GitHub 主页也记录了利用这些系统自动化处理周边猜想的尝试，填补了人类因精力有限而忽略的边缘地带。
（来源：X）
本次利用 Claude Code 进行的演示，恰恰是连接上述“前沿探索”与“日常实践”的桥梁。虽然不如谷歌 AlphaProof 解出国际数学奥林匹克（IMO）难题那般具有极高的公众戏剧性，但在 Lean 这一类型论保障的确定性环境中，陶哲轩的演示更为接地气，也更贴近当代数学家真实的研究常态。
当然，在肯定 AI 带来的效率革命的同时，陶哲轩及其代表的数学界并未回避技术现存的局限性。
一方面，学术界有声音担忧，高度依赖 AI 生成的证明可能会引入“黑箱化”问题。即便 Lean 编译器能够从逻辑底层保证代码 100% 的正确性，但长篇累牍、由机器生成的机器语言缺乏人类数学特有的直觉美感和可读性，这可能导致数学从一门“理解的艺术”异化为单纯的“符号验证”。
对此，陶哲轩保持了科学家特有的客观与中立。他倾向于将 AI 定义为一种强大的“实验数学”工具。对于高度依赖计算和模式匹配的任务，AI 无可替代；但涉及黎曼猜想这类需要颠覆性直觉和深层概念重构的核心领域，人类的主导地位依然稳固。
正如他此前在 IPAM 会议上所言：“只要 AI 为你节省的时间，多于你为了纠正它而浪费的时间，它就是一款成功的工具。”此次长达 26 分钟的无剪辑视频，正是对这一论断的最好背书。
在未来的数学研究中，“人机共作”或将成为一种新常态。届时，也许 AI 能够以“初级合作者”的身份，彻底打通数学从直觉构想到计算机形式化验证之间的瓶颈。
视频地址：https://www.youtube.com/watch?v=JHEO7cplfk8&t=124s
运营/排版：何晨龙
相关攻略
为纪念谷超豪先生百年诞辰，5月10日将在上海科技馆举办专题科普讲座。李大潜院士将回顾谷超豪从数学少年成长为学科开拓者的历程，展现其科学精神传承。沈维孝院士则以多项式求根为例，引领听众领略数学的深邃与精巧。这是一次与顶尖学者对话、感受数学魅力的难得机会。
当我们开车在高速公路上行驶时，最怕遇到的就是车子突然失控，方向盘变得异常敏感，稍微一动就可能冲出车道。这种情况在人工智能的训练过程中也经常发生，特别是在训练那些能够进行推理和对话的大型语言模型时。来
这项由威斯康星大学麦迪逊分校研究团队完成的突破性研究，发表于2026年3月的《机器学习》期刊，论文编号为arXiv:2603 20538v1。有兴趣深入了解的读者可以通过该编号查询完整论文。这项研究
这项由高通AI研究院领导的突破性研究发表于2026年3月的预印本论文，论文编号为arXiv:2603 08462v1。有兴趣深入了解的读者可以通过该编号查询完整论文。这项研究解决了一个让所有AI研究
3月31日消息，近日，比利时布鲁塞尔自由大学（VUB）数据分析实验室发布重磅研究成果，证实商用大型语言模型已具备独立生成原创数学证明的能力。OpenAI旗下ChatGPT-5 2(Thinking)
热门专题
热门推荐
华硕ROG正式发布2026款枪神、魔霸及魔霸新锐系列游戏本并开启预约。枪神系列分为标准版与超竞版，均搭载酷睿Ultra9处理器，超竞版可选RTX5090显卡并配备光显矩阵屏。魔霸系列采用AMD锐龙处理器，高配可选锐龙99955HX3D与RTX5070Ti显卡。魔霸新锐系列主打性价比，配备RTX5060显卡，面向预算有限的玩家。
内存价格高企，单通道DDR5成为高性价比装机方案，但会降低游戏性能。测试显示，锐龙59600X凭借Zen5大核架构及对内存低延迟的优化，在搭配单条DDR56000内存时，游戏性能损失较小。相比之下，酷睿Ultra200SPLUS系列更依赖高带宽，单通道下性能下滑明显。在多款热门电竞网游实测中，锐龙59600X性能领先，且整机性价比优势显著。
神牛发布ML40系列摄影灯，包含ML40Bi和ML40R两款。ML40Bi售价568元，内置锂电池，支持边充边用及NFC快速连接，侧重便携智能。ML40R售价698元，具备更广色温调节范围，侧重专业色彩控制。两者均采用磁吸设计，兼容丰富附件，满足不同布光需求。
华硕TUFGaming系列推出新款850W白金重炮手氮化镓电源，到手价849元。该电源符合ATX3 1规范，长度150mm，采用全模组设计，配备12V-2×6接口支持600W峰值功率。其获得双白金效率认证与A-噪声认证，内部使用氮化镓元件与长寿电容，搭配135mm静音风扇，并提供8年质保，主打高效、安静与持久稳定。
FalconUSD（USDF）是一种与美元挂钩的稳定币，旨在为Web3生态系统提供可靠的交易媒介和价值储存工具。其运作依赖于储备资产支持和透明审计机制，在DeFi、跨境支付等场景有应用潜力。了解其技术原理、市场定位及潜在风险，有助于理性评估这一新兴数字资产的价值与前景。