■ 风向标工作室
AI的意义就是解放人，这当然也包括解放数学家。
AI对数学界的冲击正在加速蔓延。
据新京报报道，近日，邓煜、陶哲轩等25位菲尔兹奖得主联合发布了一份名为《人工智能在数学中的严重错位》的公开声明，指出AI公司把解决数学问题当作基准测试推进，对数学共同体有害。
游说增加研究经费
这封信的导火索是，9月8日，人工智能公司Ope⁃nAI宣布用1万个智能体，花了88小时完成了Navi⁃er-Stokes千禧年难题证明。
1934年以来，这道题难住了人类顶尖数学家近90年，Leray、Nirenberg、Caffarelli、陶哲轩等一代代顶尖数学家不断逼近这个问题。2000年，它被列入七道千禧年大奖难题之一，悬赏100万美元。
其实，陶哲轩一直是利用AI研究数学的先驱者之一。这封公开信的核心，不是反对AI辅助数学，而是反对AI公司为了自己业绩、融资、股价，为了benchmark成绩刷榜，把破解数学难题当营销手段，不断抛出AI的结论，却跳过关键的“人类消化”这一步。
除了学术圈维护自己的研究传统，这封信背后还有政治动因。2027财年，特朗普政府预算提案中，科研经费呈现断崖式缩减。一些学者不得不去找大公司资助，以维持研究。
面对这样的情况，这封公开信也可看作对研究经费的游说。
AI对数学攻城略地
当然，经费问题只是表象，归根结底，是当下AI对数学的攻城略地。
2026年9月4日，Ope⁃nAI的GPT-6Astra，攻克了5道埃尔德什数学难题。仅仅过了一天，Anthropic的Claude将“费马大定理”转化为机器形式化证明。
这种攻城略地不仅表现为速度，也表现为广度。2026年9月，在一位博士后的指导下，两名高中生，借助AI工具，解决了菲尔兹奖得主许埈珥（June Huh）2022年获奖后一直未攻克的组合数学难题。
数学——“自然科学的皇冠”，正被AI以前所未有的速度，戴到了普通人的头上。在AI的帮助下，外行人也可以涉足数学的前沿领域。
AI做出了成果，如果要靠人验证，那么，基于人类能力，验证也会很慢。当下，AI频传捷报，是因为无须人类，通过软件就能验证AI做出的成果是真实的。这种软件叫作lean。
数学家的研究成果，始终可能存在逻辑错误，一处微小疏漏就会让整套论证崩塌，所以需要反复核验推导。 2013年，证明助手Lean诞生，解决了长期以来困扰数学家的这个问题。
AI的意义是解放人
数学问题，名义上被解决了，但数学界要的是解决问题过程中发现的新数学、新方法，理解和知识传承，以及把这些新东西纳入数学体系。
AI以简单粗暴的方式给出最终的答案，但人类的理解没有跟上，不仅没有开创新的数学领域和数学思想，反而可能会扼杀孕育新思想。这就是数学家的深层忧虑。
AI给出的证明，在形式逻辑上是对的，这一点有lean的保障。但这个证明是怎么干的、思路是什么，就需要人类数学家对证明进行整理和优化、总结。
AI擅长广度，人类专家则擅长深度。陶哲轩说，有经验的数学家可以判断哪些步骤是常规操作，哪些包含真正新颖的想法。
比如，数学爱好者Ma⁃zur用AI把森多夫猜想证明出来了，Lean也通过了，但稿子没人读得懂。陶哲轩在翻译的过程中，得到意外收获，覆盖了更强的猜想。
从这个角度，一定程度上，AI将会把数学的瓶颈从“想法生成”变为“验证和评估”。这需要整个数学学科的工作范式的调整、适应。
更重要的是，数学一方面是一场规则分明的形式逻辑游戏，但数学还有另外一面，那就是敢于凭空构想出一个全新的世界法则。这类探索，还需要靠人类数学家。
当然，目前数学方面开创性的研究并不多。但不多的原因，正因为人类的智慧大量地花在了形式证明上，当AI接手了这部分工作，更多的数学家就可以去从事开创性工作——AI的意义就是解放人，这当然也包括解放数学家。
□刘远举（专栏作家）
