菲尔兹奖得主警告：数学与AI公司的目标并不相同

数学界和做人工智能的公司之间的紧张，已经不再是私下议论。《世界报》刊登了一篇由二十五位菲尔兹奖得主署名的文章。菲尔兹奖是数学领域的最高荣誉。作者在文中直言，AI公司的目标和数学共同体的目标分歧很深。他们批评的不是模型能解题，而是为什么解题、又怎么对外讲述这件事。

证明不是产品

几天后，《世界报》又刊出对斯特凡·马拉的访谈。马拉是巴黎高等师范学院的数学家，2025年获法国国家科学研究中心金奖，也是JPEG 2000压缩算法的共同发明人。他的一句话成了整场辩论的题眼：AI做出的证明，如果我们没有足够的准备去理解它，本身就没什么价值。马拉研究的问题之一是多维灾难。在这个问题里，可能的构型数量增长得极快，从低维情形里找直觉已经失去意义。

这个论点可以讲得很具体。数学不只是一堆真命题，它还是一门手艺，用来理解这些命题为什么为真。验证器能确认形式化写法的正确性。可只要这些内容没有被讲解、没有被讨论，它就传不了这门手艺。

机器验证今天能做什么

与此同时，也出现了展示人与机器如何可靠协作的研究。马里奥·卡内罗在arXiv的一篇文章中证明，在Lean助手的类型论里，只需要排中律，不需要选择公理，不需要命题的外延性，不需要商，就能证明集合论ZF的一致性，而且完全形式化。这是个技术性结果，却有哲学分量。此前人们可能以为，没有选择算子，类型论的力量会明显低于ZF。

另一条路线是带验证的搜索。模型提出FunSearch风格的程序，严格的评估器给它们打分，再由选择机制留下最好的。其中一篇论文的作者甚至用笔记本电脑做实验，本地模型为三百亿参数，每次运行有120到600个经过验证的样本。结果有两面，因此更有价值。在旗舰任务上，搜索填平了略超过90%的差距后停住。而当给模型一个关于构造族的提示时，整个循环优化了给出的想法，尽管任何一次独立运行都没有发现它。

背后仍是激励问题。如果最重要的标准变成榜单上的纪录，数学就变成一组基准，而不是一种理解的实践。对这种简化的警惕并非敌视工具，而是让工具能长期有用的条件。