--- layout: post.njk source: https://yage.ai/share/tao-lean-formalization-credibility-20260623.html speaker: yage.ai title: 当陶哲轩说AI跨过了数学形式化的临界点 date: '2026-06-23' summary: 文章探讨了数学家陶哲轩关于AI在形式化任务中突破临界点的判断。核心观点在于区分了AI生成证明的‘正确性’（第一层门槛，AI已达）和‘工程可用性’（第二层门槛，AI仍存在瓶颈）。作者认为，真正的拐点在于解决了如何将正确的数学结果组织成可维护、可复用的知识体系这一更高抽象层面的问题。 area: tech-engineering category: ai-application tags: - formalization - proof-verification - knowledge-organization - llm-limitations people: - 陶哲轩 companies_orgs: [] products_models: - Lean media_books: [] draft: true status: evergreen --- 2026年6月21日，陶哲轩在Mathstodon上发了一篇帖子。他说过去几周里，自己在IEANTN项目里发出去的形式化任务，几乎全部由AI在几小时内完成。同样的任务几周前还需要懂数论又会Lean的志愿者花几周认领。IEANTN由IPAM UCLA主持，全称Integrated Explicit Analytic Number Theory Network，目标是把解析数论中大量繁琐的数值核对工作搬进Lean证明助手，建成一套可维护、可更新的估计网络。他还提到另一面：AI生成的证明比人写的长几百行，代码冗余，抽象层级常常选错，人去阅读和整理这些结果反而成了新瓶颈。第二天，中文科技媒体编译了这条消息，标题写的是AI突破临界点、数学家被淹没。[原帖] 两边的说法差得有点远。这篇文章要回答一个可信度问题：陶哲轩这次究竟是一声低阈值惊呼，还是一个经得起检验的判断？把他的原帖、他过去三年在这个方向上的公开态度、同行的反应和独立的外部证据一起摊开，结论偏后者。但原因不是那个几周缩到几小时的速度数字本身。他这次讲的其实是一件事的两层，我们只听到了一层。’AI生成快、人消化慢’这个现成概括一出来就把剩下那层盖住了。 ## 先把”拐点”到底是什么讲清楚 几周变几小时，AI生出的证明又长又冗余，人消化不过来。这三件事放在一起，读者的第一反应很自然：这不就是AI写代码那套陈词滥调吗？AI堆屎山、code review跟不上，软件工程圈讲了至少三年了。如果陶哲轩只是在重复同一个判断，这篇文章就不用往下写了。所以得先把这个问题拆开。 区别在于，他说的”对”其实有两层，他这次报告的拐点只穿过了其中一层。 打个比方。一份代码，能跑通测试，是一回事；写得干净、别人能看懂、能拿来改、能并进主干长期维护，是另一回事。数学形式化里也有同样的两层。 第一层是证明本身有没有错。IEANTN要把解析数论里的数值核对搬进Lean这种形式化工具里——你可以把Lean理解成一个对数学证明做自动批改的编译器，证明对错不由人判断，由它裁定，而且它只认机器能验证的逻辑，没有商量余地。陶哲轩自己说过，这类数值核对占他思考数论问题时间的三分之二以上。[项目页] 这一层之前有一道硬门槛：要既懂数论又懂这套形式化语言的志愿者，花几周做一个。现在AI几小时做完，批改器确认无误。学术界专门有人做评测时还加了防作弊检查，确认AI没有偷懒跳过步骤，才算通过。[arXiv 2606.05632v1] 所以陶哲轩说任务被清空，不是AI自己声称完成了，是机器逐行确认了正确。在一个门槛这么高、之前公认要靠专业人类的环节上，第一层被AI拿下了。这和”AI写代码快”不一样，因为门槛不一样。 第二层是这份通过批改的证明，能不能真正用起来。证明没错，不等于它写在合适的抽象层级上，不等于后面的人能直接拿来用，也不等于整个数学知识库不会因为它越堆越乱。这一层AI做得相当差，而且因为第一层通了，第二层反而更卡。arXiv 6月一篇报告（2606.13925v1）记下了一次完整的专家审查：Claude Code把一个代数几何定理做了形式化，机器批改通过，专家看完发现一堆毛病。[arXiv 2606.13925v1] 比如，AI为了把任务做完，该证明A=B的时候，发现只证一个弱化版本（如果A是零那B也是零）就够交差，于是偷了个懒，走捷径省事，但这个捷径让证明没法被别处复用。它还会自己造一些没必要的定义，把知识库里已经存在的东西换个名字重新命名一遍，反而让整个系统更难用。证明本身写得密密麻麻、中间步骤堆成一面墙，专家读完很费劲。专家的概括是，AI把眼前的局部目标关掉很在行，但要决定整个证明里应该有哪些对象、怎么组织，这一层做不了。 陶哲轩自己把这两层分开在讲。他说的拐点，是第一层（证明没错）打通了。他提到的”阻抗不匹配”，是第二层（证明能用）成了新瓶颈。这个分层才是他判断里真正有信息量的地方。把两层压成一层来讲，就降格成了代码屎山的又一个翻版。 ## 一个审慎的人花了三年才走到这个判断 新模型一发布就喊拐点，陶哲轩不做这种事。过去三年，他在这个方向上的公开判断一直偏谨慎。2025年，他对LLM的定位是’过度自信的本科生’：想法会提，好赖辨不出来。2026年3月，他在一篇长文里把AI在数学前沿的边界画得更清楚：前沿领域没有现成的发表物和训练数据做底子，LLM到了那个地方就失效。[WordPress] Quanta Magazine六月那篇人物特写专门提到了这一点：陶哲轩是先看清了AI做不了什么，然后才转了态度。[Quanta] Quanta用来形容他的词是谦逊和低调。一个被专业媒体这样描述的人，在自己亲手推进的项目里看着任务从几周缩到几小时，然后说出’拐点’。这句话的分量，和一个追逐流量的博士跳出来喊’突破’，是两回事。 同期的数学界氛围，让他的审慎显得更有分量了。2026年6月2日，几十位数学家联署了一份声明，标题只有三个词：别信炒作（Don’t Believe the Hype），要求停止对AI数学能力的不实宣传。哥伦比亚大学的Michael Harris在Phys.org的报道里直接向陶哲轩发难，说他最近公开替OpenAI背书，总让同一个人出来替整个数学界说话，这本身就有问题。[Phys.org] 陶哲轩在数学界的位置很特殊：他是愿意公开站到厂商那一边背书的人里分量最重的，此刻正顶着同行的现实压力。在这种气氛里，他没有收回任何话，继续在自己主持的项目里报告实测数据中看到的拐点。他在这个压力下也没改口，这件事本身说明，他在自己项目里看到的东西，不是几句简单质疑就能消掉的。 ## 不止他一个人看到了这两层 这同一个模式，独立验证也在增长。前面提到的那篇arXiv 2606.13925v1不是孤例。它记录了一个Lean校验通过的证明，在工程可用性上大面积丢分的过程，正好坐实了陶哲轩说的那句：全局重构超出了AI目前的能力。 Kevin Buzzard是Lean社区最核心的推动者之一。他在Physics World关于Erdős问题的辩论里反复划同一条线：AI拿着已知技巧能做很多事，但这里和生成新思想是两件事。[Physics World] David Bessis说得更直接，把现阶段AI形式化叫作AI粗制滥造。两边分歧在评价色彩上，不在对事实的共同认定上：所有人都同意，生成那一侧加速之后，工程可用性这一侧严重滞后了。 斯坦福5月的Future of Mathematics Symposium上，陶哲轩专门挑出一个风险来提醒：LLM把有深度的推理和例行步骤放在同一个平面上处理，显式目标和隐含目标之间的张力，模型分辨不出来。[Substack] 一个证明里，每一步语法上都站得住，但哪一步真正扛着数学洞察、哪一步只是走过场，模型一视同仁。这和他在IEANTN里实际碰到的情况，是同一件事。 生成端提速、消化端跟不上，这个模式不只数学有。软件工程里，GitHub Copilot之后代码生成成本跳水，code review的工作量不降反增。文本生产里，生成端到了秒级，fact-checking的工时几乎没有变化。设计流水线里，候选方案的产生成本趋近于零，筛选和调整的成本原地不动。这些不是数学独有的问题。但陶哲轩在数学一线给出的分层判断，比这些领域里’生成快、消化慢’的笼统说法精确得多：他指出了哪一层突破了、哪一层没有。 ## 他说的是已知道路的提速，不是发现新路 边界要放在明面上。陶哲轩报告的临界点，是工程化形式化的临界点，不是原创证明的临界点。IEANTN里要验证的东西，答案已经是知道的。要解决的是找一个更系统的方式，把它表达出来、维护起来。前沿数学的原创推进，从零构造新定理，铺出新的论证路径，决定往哪个方向翻，仍然在他反复标出的能力边界之外。他说的拐点，是路已经有人铺好了，从慢走变成了快走。让AI自己去找一条没人踩过的路，那是另一个问题。