AI可能会完全改变我们的数学方式

人工智能革命是要改变数学吗？得益于自动化工具，一些著名的数学家这样认为，可以帮助写证明突然表现出令人印象深刻的能力飞跃，并有可能改变数学研究的方式。

全球大约100名顶级数学家在6月聚集在剑桥大学举行了一次会议，其主题是基于计算机是否可以帮助数学家解决了一些长期存在的问题，即如何检查他们的证据是否正确。这个过程，称为形式化，不一定必须涉及人工智能，实际上，2017年在剑桥举行的类似会议也没有提及AI。

但是八年后，人工智能突飞猛进，最著名的是，大型语言模型为诸如chatgpt这样的工具提供了成功。这引起了人们对AI可能如何影响数学的问题的新兴趣从自动将人写的证明转化为正式的，可检查的语言，本身构建证据。

这有点不知所措。杰里米·阿维加德（Jeremy Avigad）在宾夕法尼亚州的卡内基·梅隆大学（Carnegie Mellon University），他们帮助组织了会议。很好；我已经做了很长时间了，它曾经是一种边缘，利基市场。突然之间，我发现自己很受欢迎。

Google DeepMind进行了两个会谈，去年，当它的AI系统（字母防止），该会谈成为头条新闻。达到了银国际数学奥林匹克运动会（IMO）的奖牌得分，这是一项享有盛誉的年轻数学家竞争，也是AI系统的长期目标。•如果您与数学家交谈并询问他们有关[字母防imo]结果，那么您将会有不同的反应。我认为大多数人会说这是非常困难的高中问题，但也许其他一些数学家会称它们为琐事。托马斯·休伯特，DeepMind的研究工程师。

休伯特（Hubert）和他的团队表明，字母防护可能超越了IMO竞争，以帮助正式化质量数字定理的一小部分，这是数字理论的重要成果。数学已经转换为“精益”，一种编程语言，但是字母隔板能够证明该定理，然后检查它是正确的。休伯特说：“我想对现实生活中如何使用字母隔板的演示。”

总部位于美国的AI创业公司Morph Labs也展示了一种名为Trinity的AI工具，该工具旨在完全自动翻译证明，从手写的数学符号开始，并在Lean中生成完全正式和检查的证明。Bhavik Mehta在伦敦帝国学院，曾与Morph Labs进行了咨询，展示了三位一体的例子，证明了与ABC猜想有关的定理，该定理臭名昭著仍然是关于它是否真实的激烈辩论的主题形式化可以解决的问题。

尽管此证明只是ABC猜想所需的整个证明的一个小构建块，而三位一体则需要比原始纸张更详细的手写版本，但许多人惊讶于该工具生成了多少正确的数学代码。

``Morph所做的事情与以前发生的事情之间的区别是，他们拿了整个数学纸，尽管从1962年起只有四页，但人类（然后）将论点分为小块，然后一台机器将整个东西翻译成瘦肉，”说。凯文·巴扎德（Kevin Buzzard）在伦敦帝国学院。我不确定我们以前看过类似的东西。

但是，梅塔说，这仍然不清楚这对其他数学领域的作用。这本质上是第一次尝试，第一次尝试起作用，也许很幸运。

Morph Labs的Christian Szegedy声称，一旦该工具完全启动并运行，它将很快进步。``一旦建立了反馈循环，我们就不需要该定理所需的手持量。然后，它基本上变成了链反应，我们可以立即完成所有数学。”

这样的工具已经正处于可能对数学家的帮助下。蒂莫西·高斯（Timothy Gowers）在剑桥大学。``这只会花一些工作来创建它们，而且似乎有很多人热衷于做到这一点，所以我认为在接下来的几个中，我真的很少有一到五年的任何事情，无论我们做数学的变化都会改变，而我们的数学方式将在重要的数学上与数学上的变化相媲美，这些变化是通过电子邮件，乳胶的数学范围[] ands late ands ands anders anders anders anders andiv and repotive []

但是，并非所有的数学家都同意，《变形实验室》论文是如此令人印象深刻。Rodrigo Ochigame在荷兰的莱顿大学，我们警告说，我们不知道作品的全部细节。他们在没有写论文或共享有关其方法的基本信息的情况下仅发布了系统的单个，可能是樱桃的输出。他们说，他们甚至没有说是否在任何其他定理上测试了他们的系统。当受众询问模型使用的计算量时，他们反复拒绝回答，因此很难评估其结果的重要性。

怀疑仍然是关于AI工具的有用程度。大多数数学家仍然没有使用自动化工具，目前尚不清楚他们是否会随着工具的改善而改变主意。Minhyong Kim在英国国际数学科学中心。数学和数学家的倾向非常多样化。我想有些人最终会非常有效，创造性地使用AI工具，而有些人会尝试保持距离。

Ochigame说，人们低估了数学研究的复杂性，创造力和微妙性，这就是为什么仍然使用笔，纸和深思熟虑进行如此大量研究的原因。他说：“高中数学比赛（例如IMO）和尖端研究之间存在巨大差距。”