数学圈子这两年的动静，实在有点大。2026年9月，Anthropic对外公布，Claude耗时11天完成费马大定理的形式化证明，产出约1300万行Lean代码，一共证明3.03万个定理。帝国理工学院的Kevin Buzzard早前预估，这项工作交给人类，要耗费十年。他本人也牵头了一个专门针对费马大定理的MathLib扩展项目。Buzzard审阅完Claude产出的内容之后，说了一句值得琢磨的话，从前他对怀尔斯的证明有99.9%的把握，看过这份成果之后，确信度直接拉到百分之百。多伦多大学的Daniel Litt说得更加直白，如果AI可以完成费马大定理的形式化工作，那它大概率能对各类数学命题做形式化处理。
但有一点需要分清，AI并没有重新证明费马大定理，怀尔斯早在1995年就完成了这项证明。AI做的工作，是把这套证明翻译成计算机能够逐行核验的形式化代码。形式化和推导证明本身，完全是两件事。形式化就是把人类用自然语言写的证明，拆成Lean能够校验的每一步逻辑。人类数学证明里大量“容易看出”“同理可得”这类省略表述，放到形式化流程里面，必须全部补齐。过去这类工作只能人工完成，耗时长，工作量巨大，现在AI能够接手，效率高出人类好几个数量级。
真正触动数学家群体的，不是这单独一件事，而是背后显现出来的趋势。2025年夏天，多款AI模型参与IMO竞赛，六道题目解出来五道。IMO题目难度再高，终究是有标准答案的竞赛题，和原创数学研究不是一回事。不过2025年一整年，不少数学家发现，AI已经不单单能做题。陶哲轩接受Quanta Magazine采访时提到，2025年AI在各类数学任务上，才真正具备实用价值。他和DeepMind合作开发AlphaEvolve系统，在67个数学研究问题上开展测试，部分问题的求解速度，比人类数学家快几十倍。陶哲轩打了个比方，一人拿着铲子，一人握着镐，互相配合才能打通隧道。
陶哲轩之后在斯坦福开展演讲，演讲结束，他做了一个决定，不再实时跟进所有新产出的证明。他原话提到，数学正在从证明稀缺阶段，转入证明过剩的阶段，AI生成证明的速度，远远超过人类阅读核验证明的速度。Erdős问题网站积压了大约20篇借助AI完成的解题方案，提交者坦言没有空余时间手动核验。陶哲轩拿19世纪汽车做类比，车辆速度持续提升，道路配套跟不上，最终没有实现通行提速，反而造成拥堵。
这里随之出现一个很现实的矛盾。AI生成的证明，很多时候不是数学家想要的那一类。陶哲轩用“阻抗不匹配”来形容这个现象。AI产出的形式化证明，比人类撰写的多出数百行，充斥大量冗余步骤，不少引理放置的抽象层级并不合适。Claude生成的29500个中间定理，Buzzard评价其中一部分可以整合进MathLib，但需要投入巨大工作量。他还提出警告，如果每一个AI项目都单独搭建一套Lean库，数学界会陷入糟糕的局面，多套互不兼容的形式化库并行存在。
数学家群体内部看法并不统一。2026年6月，十六位数学家共同起草《莱顿宣言》，警示AI正在冲击数学成果的可靠性、署名规则，还有研究者自主探索的空间。这份宣言已经收获全球六百多名数学家签名支持，国际数学联盟也予以背书。菲尔兹奖得主Peter Scholze在宣言里态度很明确，思考数学问题不会使用AI，也尽量不去阅读AI生成的文本。有意思的是，Buzzard本人同样支持这份宣言。也就是说，深度参与AI形式化项目的研究者，也认同要给AI的使用划定边界。
那数学领域到底有没有发生本质改变。站在工具角度，变化确实不小。形式化验证的提升实实在在，清华大学FormaTheoria项目借助AI辅助，推进有限单群分类这套两万页的证明，产出超过99.4万行Lean代码。效率提升不是小幅上涨，是数量级的跨越。从前一个人花费数月完成的任务，如今几天就能做完。数学家的工作节奏必然受到影响。
但“彻底变革”这个说法，要拆开看待。工具更新之后，数学研究部分环节效率暴涨。可数学核心的问题没有变化。哪些问题值得深挖，哪个方向具备潜力，什么样的证明称得上简洁优美，这类判断AI做不到。陶哲轩演讲把数学工作流程划分成三段，证明生成、证明验证、证明阐释。AI在前两项能力很强，第三项几乎无法参与。一份证明的结构，推导逻辑，以及它和其他数学分支之间的关联，依旧需要人类梳理讲清楚。
另一名菲尔兹奖得主Akshay Venkatesh，观点相比陶哲轩更为谨慎。他承认AI带来巨大影响，但有些根植于学科文化里的珍贵东西，需要尽力保留。他担心，如果数学家习惯依靠AI产出证明，只查看最终结论，代代传承下来对于数学结构的直觉感知，会慢慢断裂。这种顾虑并非凭空而来。学生依靠AI做完习题，拿到正确答案，脑海里却建立不起对应的理解。
中科院数学与系统科学研究院的研究员高小山，表述比较务实。未来AI会成为数学家的标配工具，研究效率或许提升数倍甚至十倍，之后菲尔兹奖相关成果大概率会有AI参与，但主导权依旧掌握在人类手上。听起来像是常规表述，细细琢磨能够成立。AI可以生成、核验证明，检索海量文献寻找关联，但是它不会判断哪个问题有意思，不会在一个方向钻研十年发现行不通之后，决定转向别的赛道，不会在深夜突然联想到不相干的类比。这些内容，是数学研究最难自动化、不可替代的部分。
综合来看，数学领域正在改变，但距离彻底变革还差很远。准确来讲，是数学研究的工作模式被改变，数学本身的核心问题没有变。AI帮数学家卸下大量机械劳动，形式核验、文献检索、繁琐推导，这些工作交给AI没问题。可数学家省出来的时间用来做什么，是新的难题。如果继续用来处理更多机械任务，只是单纯加快工作节奏。如果投入更深层次的思考，才算是真正的提升。陶哲轩选择不再追着所有新证明看，本质就是做出这个取舍，放弃广度，把精力留给方向判断。
还有一个值得持续关注的变量，AI能不能独立提出有研究价值的全新猜想。目前还做不到。AI可以证明埃尔德什猜想，解答IMO题目，完成费马大定理的形式化，但是没有相关报道提到，AI独立提出过让数学家觉得值得深挖的猜想。提出猜想需要研究品味与直觉，还要感知整个数学体系的结构，现阶段没有证据证明AI拥有这类能力。如果哪天AI做到这件事，才是真正需要警惕的时候。现阶段，它只是好用的工具，好用到人们偶尔会忘记，它终究只是工具。
