陶哲轩转发、菲尔兹奖得主领衔：AI正在颠覆数学家的工作方式 | 美国数学学会特刊

文章来源：量子位

陶哲轩点赞转发，《美国数学学会通报》用一整期特刊介绍了AI给数学带来的改变。

这些文章读起来很有趣，尽管使我自己即将发表的一篇文章显得多余……这个领域发展太快了！

作者阵容非常豪华，包括菲尔兹奖得主Akshay Venkatesh、华裔数学家郑乐隽、计算机科学家Ernest Davis等多位知名学者。

其中郑乐隽表示，如果最终机器能做得比人类更好，那很好，她将乐意退出数学领域去弹钢琴。

他们提出的观点包括：

AI的数学能力不完全反映人类的认知过程，依赖于训练数据中的模式，而不是真正理解问题的本质。
合成数学如合成拓扑学和合成微分几何学，提供了一种全新的数学实践方式，允许数学家专注于更深层次的概念和问题。
交互式证明系统与软件工程中的“规范驱动开发”，可以降低数学家的认知负荷、促进数学家之间的合作。 形式化证明技术可能改变数学证明的本质、颠覆数学家的工作方式。 数学届不应被科技公司主导的议程所绑架。

在开篇，编委会写道：

纯粹的数学家习惯于享有很大程度的研究自主和智力自由，这是一种脆弱而宝贵的遗产，可能会因机器的盲目使用而被扫除。
另一方面，对同一技术进行深思熟虑和深思熟虑的方法可能会极大地丰富我们的学科。
学科应该如何发展是由我们自己决定的，因此我们邀请数学界认真思考和讨论专刊中提出的问题，并聆听其他领域同行对这些问题进行了深入思考。

现在，是数学家们了解并推动这场辩论，并决定学科未来方向的时候了。

AI能自动证明定理吗？

计算机已经在数学中发挥了重要作用，尤其是在计算效率方面的提升，但是否能够帮助人类进行数学推理？有一天它们是否会自主进行推理？

数学家Kevin Buzzard概述了神经网络、计算机定理证明器和大型语言模型的最新发展。

Kevin Buzzard现任英国伦敦帝国理工学院数学教授，他专门研究算术几何和朗兰兹纲领。

回顾整个计算工具的历史，最早Computer一词还指人类作为“计算员”，他们的成就不应被低估。

17世纪早期，苏格兰数学家John Napier构造了第一个对数表，他提出如果有更多“计算员”来帮忙，就可以进一步推进这一工作。

另一个代表性成果是Felkel和Vega在18世纪70年代发表的整数因式分解表，这使研究素数分布成为可能，最终导致了素数定理的证明。

早期电子计算机出现后，机器在高速计算方面已经远超人类，Computer一词的含义也发生了变化。

如剑桥大学在1957年购买了EDSAC II计算机，用于海洋学计算，为现代板块构造理论奠定基础。

这个阶段计算机还只是一个工具，即使目前的计算机也难以像人类一样进行数学推理和定理证明。

神经网络可以用于搜索定理、猜测新定理和寻找反例，如发现了拓扑学中关于结点和边的关系的新定理，以及在表示论中发现了关于Kazhdan-Lusztig多项式的新结果，但对于证明深奥复杂的定理还有局限性。

自动定理证明系统（ATP）可以自动证明一些复杂的定理，如罗宾斯猜想。但ATP生成的证明往往过于冗长，难以被人类理解。

交互式定理证明系统（ITP）可以用于验证定理的正确性，帮助发现和修正数学文献中的错误，如数学家Peter Scholze在液体张量实验（Liquid Tensor Experiment）中承认自己无法掌握所有涉及的数学对象和概念，最终在Lean系统帮助下完成。