AI军火商正在把数学家的黑板变成算力跑分场。
2026年10月16日，Jeremy Avigad、Kevin Buzzard等7位数学形式化领域的领军学者在Xena Project联合刊发檄文，正面回应近期OpenAI、Anthropic和Math, Inc.掀起的大规模数学形式化浪潮。学者们给出的判断极为严厉：如果放任AI巨头不顾可读性与人类理解、只求速度地堆砌形式化证明，不仅不会加速数学发现，反而会留下数以千万行无人能用的机器废料，让该领域遭遇持久倒退。
机器交卷与通胀的正确性
冲突源于科技公司最近接连扔出的一系列重磅炸弹。2026年9月4日，Anthropic宣布Claude在短短11天内产出1300万行Lean代码，形式化验证了费马大定理（FLT），中途证明了多达29,500个中间定理。在此之前，OpenAI公布了纳维-斯托克斯方程爆破解的自然语言证明与Lean形式化成果；初创企业Math, Inc.也突击介入球堆积形式化项目，宣称其模型Gauss在私有fork中写出50万行代码覆盖24维空间。
从计算机科学的角度看，这些都是惊人的里程碑。代码全部通过证明助手的编译器检查，没有任何作弊，也没有留下未完成的占位符。但在专业数学家眼里，这些庞然大物更像是一座座难以逾越的代码垃圾堆。
编译通过不等于数学知识，没有抽象价值的证明不过是机器废纸。
在形式化证明中，定理被转译成严格的计算机代码。但费马大定理本身在数学界早已没有真伪悬念，形式化的唯一价值在于人类能否通过重构证明，提炼出优雅、模块化且能供后续研究调用的通用工具。然而，Anthropic的1300万行产物几乎不具备这种价值。即使Kevin Buzzard公开肯定了Claude的技术突破，他依然明确表态：自己团队由人类主导、追求现代数学表达与清晰架构的费马大定理形式化项目绝不终止。
机器完成了证明，但人类什么也没学到。
飞车式证明与生态掠夺
更严重的问题在于工程维护成本与社区规则的破坏。2026年2月23日，球堆积形式化项目刚宣布达成8维证明的里程碑，Math, Inc.便利用AI补全证明，直接将主干代码量从2万行粗暴推高到8万行。项目团队在技术审查中发现，这些自动生成的代码充斥着缺乏模块化设计的微小辅助定义、数百行极易失效的脆弱长代码，甚至在大规模重复制造Mathlib中早已存在的公理。
维护团队最后不得不将这批代码重构并缩减至6万行，甚至坦言：清理AI代码的难度，远比自己动手重新写一遍还要高得多。数学界将这种行为讽刺为飞车式证明（drive-by proving）。
AI大厂并非在真空中完成突破。Claude对费马大定理的突击，高度依赖Buzzard团队长期在flt-regular项目上积累的基础定义；Math, Inc.也是在学界搭好前九成脚手架后，才完成了最后冲刺。大厂摘取成果用于技术宣传，却把维护和消化的重担全甩给了学术共同体。OpenAI甚至在其纳维-斯托克斯方程的代码库中直接倾倒了大量非自然语言可读的文件，后续部分结论出现撤回，非形式化文本与形式化代码存在多处脱节，极大地消耗了研究者的信任。
- 风险.AI巨头将开源数学库视为免费的数据提炼工场，若放任缺乏同行评审的机器代码倾倒，将直接挤垮Mathlib等依赖志愿维护的学术生态。
寻找人机共生的防火墙
面对算力倾销，数学家并非全盘排斥技术，而是试图筑起一道工程准则的防火墙。学者们指出了正反两面的先例：OpenAI对单元距离猜想的证伪、Anthropic关于黎曼zeta函数零点密度的成果，都因提供了坚实的数学理解而受到赞许。真正的分水岭不是用不用AI，而是由谁来定义标准的对齐问题。
为了对抗混乱的代码倾倒，学界正在推进更有秩序的试验。例如获得开源科学大奖的Mathlib，至今依赖65位审查员与950位贡献者的人工维护，宁慢勿滥；Kevin Buzzard主导的Annals挑战赛，专注补全顶刊论文中的核心数学定义，引导研究者把力气花在刀刃上。
而在自动化方向，Tau Ceti项目探索出了一条新路：由人类数学家划定严密的技术路线图，让AI生成证明，再由其他AI依照复用性、命名规范、抽象泛化程度进行对抗性互审。Tau Ceti代码量已达300万行，成功涵盖了黎曼-罗赫定理与舒尔-韦伊对偶等深水区成果，并始终无缝对接Mathlib的架构标准。另一边的Formal Frontier项目也在探索教材批量管线，产出包括毛球定理、嘉当定理等在内的41个可复用模块。
- 结论.形式化数学的根基不是计算力，而是概念框架。如果机器生成的证明无法成为后续定理的脚手架，数千万行代码也不过是一场徒增维护成本的虚假繁荣。
数学不需要不可读的万寿寺，它需要能被后来者继续攀登的阶梯。