人工智能将成为数学家的“副驾驶”
数学传统上是一门独立的科学。1986年，安德鲁·怀尔斯为了证明费马定理，退到书房里呆了7年。由此产生的证明往往很难让同事们理解，有些至今仍有争议。但近年来，越来越多的数学领域被严格地分解为各自的组成部分(“形式化”)，证明可以由计算机进行检查和验证。
加州大学洛杉矶分校的Terence Tao相信，这些方法为数学领域的合作开辟了全新的可能性。如果再加上人工智能的最新进展，未来几年该领域可能会出现全新的工作方式。在计算机的帮助下，尚未解决的大问题可能更接近于解决。陶在接受《科学美国人》的德语姊妹刊物《光谱》(spectrum der Wissenschaft)采访时阐述了他对未来的看法。
[以下是经过编辑的采访实录。]
在你在旧金山联合数学会议上的一次演讲中，你似乎暗示数学家之间并不相互信任。你这话是什么意思?
我是说，我们有，但你得认识个人。除非你能逐行检查他们的工作，否则很难与素未谋面的人合作。通常情况下，5个是合作者的最大数量。
随着自动校验器的出现，这种情况是如何改变的?
现在你可以和几百个你从未见过的人合作。你不需要信任他们，因为他们上传代码，Lean编译器会验证它。你可以做比我们通常做的更大规模的数学。当我用所谓的多项式Freiman-Ruzsa (PFR)猜想形式化我们最近的结果时，[我和]20多人一起工作。我们把证明分解成很多小步骤，每个人都对其中一个小步骤做出了证明。我不需要逐行检查贡献是否正确。我只需要管理整个事情，确保一切都朝着正确的方向发展。这是一种不同的数学方法，一种更现代的方法。
德国数学家、菲尔兹奖得主彼得·肖尔兹(Peter Scholze)参与了一个精益项目——尽管他告诉我他对计算机了解不多。
对于这些形式化项目，并不是每个人都需要成为程序员。有些人只关注数学方向;你只是把一个大的数学任务分成很多小的部分。还有一些人专门研究将这些小片段转化为正式的证明。我们不需要每个人都是程序员;我们只需要一些程序员。这是一种分工。
我在20年前就听说过机器辅助证明，当时它还是一个非常理论化的领域。每个人都认为你必须从头开始——将公理形式化，然后做基本的几何或代数——而进入高等数学超出了人们的想象。是什么改变了形式数学的实用性?
有一件事发生了变化，那就是标准数学库的发展。尤其是Lean，它有一个叫做mathlib的大型项目。所有本科数学的基本定理，如微积分和拓扑学等，都被一个接一个地放在这个图书馆里。因此，人们已经投入了工作，从公理到一个相当高的水平。我们的梦想是让图书馆达到研究生的教育水平。这样，(数学的)新领域的形式化就容易得多了。也有更好的搜索方法，因为如果你想证明一些东西，你必须能够找到那些已经被证实是真的东西。所以智能搜索引擎的发展也是一个重要的新发展。
所以这不是计算能力的问题?
不，一旦我们正式确定了整个PFR项目，只花了半个小时来编译验证。这不是瓶颈，而是让人们使用它，可用性，用户友好性。现在有一个成千上万人的大社区，还有一个非常活跃的在线论坛来讨论如何使语言变得更好。
精益是最先进的还是存在竞争系统?
精益可能是最活跃的社区。对于单个作者的项目，也许有一些其他的语言稍微好一些，但是总的来说，Lean更容易上手。它有一个很好的图书馆和一个很好的社区。它最终可能会被另一种语言所取代，但现在它是占主导地位的形式语言。
当你做一个关于另一个数学项目的演讲时，有人问你是否想把它形式化，你基本上说这需要很长时间。
我可以把它正式化，但要花我一个月的时间。现在，我认为我们还没有达到将一切例行公事形式化的地步。你必须挑选。你只想把那些真正对你有用的东西形式化，比如教你如何在精益中工作，或者其他人是否真的关心这个结果是否正确。但这项技术会越来越好。所以我认为在很多情况下，更明智的做法是等待，直到它变得更容易。它不需要花费10倍的时间来形式化，而是花费传统方法的两倍的时间。
你甚至说过要把这个因子降到小于1。
有了人工智能，就有可能做到这一点。我想在将来，我们会向一些GPT解释它们，而不是打印我们的证明。GPT会尝试在精益中将其形式化。如果一切顺利，GPT就会说:“这是你用LaTeX写的论文;这是你的精益证明。如果你愿意，我可以按下这个按钮，帮你把它提交给杂志。”它将来会是一个很棒的助手。
到目前为止，证明的想法仍然来自人类数学家，不是吗?
是的，最快的形式化方法是首先找到人类的证据。人类提出的想法，证明的初稿。然后把它转化为形式证明。在未来，也许事情会有所不同。可能会有一些合作项目，我们不知道如何证明这一切。但是人们有关于如何证明小片段的想法，他们将其形式化，并试图将它们组合在一起。在未来，我可以想象一个大定理是由20个人和一群人工智能共同证明的，每个人工智能都证明了一些小事情。随着时间的推移，它们会连接起来，你就可以创造出一些奇妙的东西。那太好了。这甚至要等很多年才能实现。技术还没有到位，部分原因是目前正规化太痛苦了。
我曾与一些人交谈过，他们试图使用大型语言模型或类似的机器学习技术来创建新的证明。Tony Wu和Christian Szegedy最近与Elon Must等人共同创立了xAI公司，他们告诉我，在两到三年内，数学将像解决国际象棋一样被“解决”——机器将比任何人类都更擅长寻找证明。
我认为三年内人工智能将对数学家有用。这将是一个伟大的副驾驶。你试图证明一个定理，你认为有一步是正确的，但你不太清楚它是如何正确的。你可以说，“人工智能，你能帮我做这些事吗?”它可能会说，“我想我可以证明这个。”我不认为数学会被解决。如果人工智能有另一个重大突破，那是有可能的，但我想说的是，在三年内，你会看到显著的进步，人工智能的实际应用将变得越来越容易管理。即使人工智能可以完成我们现在所做的数学运算，这也意味着我们将会进入到一个更高类型的数学。现在，举个例子，我们一次证明一个。这就像一个个工匠在做一个木制娃娃或别的什么东西。你拿一个娃娃，仔细地把所有的东西都涂上，以此类推，然后你拿另一个。我们做数学的方式并没有太大的改变。但在其他学科中，我们都有大规模生产。所以有了人工智能，我们可以一次证明数百或数千个定理。人类数学家将指导人工智能做各种事情。所以我认为我们做数学的方式会改变，但他们的时间框架可能有点激进。
2018年彼得·舒尔茨获得菲尔兹奖时，我采访了他。我问他，有多少人明白你在做什么?他说大概有10个人。
在形式化项目中，我们注意到的是，你可以与那些不了解整个项目的全部数学原理的人合作，但他们只了解其中的一小部分。就像任何现代设备一样。没有一个人可以自己造出一台电脑，开采所有的金属，提炼它们，然后制造硬件和软件。我们有所有这些专家，我们有一个庞大的物流供应链，最终我们可以创造出智能手机或任何东西。现在，在数学合作中，每个人都必须了解几乎所有的数学知识，正如[Scholze]提到的那样，这是一个绊脚石。但是有了这些形式化，就有可能只知道其中的一部分就对项目进行划分和贡献。我认为我们也应该开始将教科书正规化。如果教科书是形式化的，你可以创建这些非常互动的教科书，在那里你可以描述一个结果的证明，在一个非常高级的意义上，假设有很多知识。但是如果有你不明白的步骤，你可以扩展它们并进入细节——如果你愿意的话，一直到公理。现在还没有人在教科书上这么做，因为工作量太大了。但如果你已经把它形式化了，电脑可以为你创建这些互动教材。这将使一个领域的数学家更容易开始为另一个领域做出贡献，因为您可以精确地指定一个大任务的子任务，而不需要了解所有内容。
数学证明不仅仅是检查某件事是否正确。证明也是关于理解的，对吧?有漂亮的证明，也有非常技术性的丑陋证明。好的证明能使你对问题有更好的理解。所以，如果我们把这个任务交给机器，我们还能理解它们所发现的东西吗?
数学家所做的是我们在探索什么是真，什么是假，以及为什么事情是真的。我们的方法是通过证明。每个人都知道，当它是真的，我们必须去证明它或反驳它。这要花很多时间。它是乏味的。但在未来，也许我们会问人工智能，“这是真的还是假的?”我们可以更有效地探索空间，我们可以试着专注于我们真正关心的事情。人工智能将通过加速这一过程来帮助我们。我们还会继续开车，至少现在是这样。也许50年后情况会有所不同。但在短期内，人工智能将首先自动化无聊、琐碎的工作。
人工智能会帮助我们解决数学中悬而未决的大问题吗?
如果你想证明一个未解决的猜想，你需要做的第一件事就是把它分解成更小的部分，每一个都有更大的机会被证明。但是你经常会把一个问题分解成更困难的问题。把一个问题转化为一个更难的问题比转化为一个更简单的问题容易得多。在这方面，人工智能并没有表现出比人类更好的能力。
通过分解问题并探索它，你也会在这个过程中学到很多新东西。例如，费马大定理，是一个关于自然数的简单猜想，但是用来证明它的数学不再是关于自然数的了。所以解决一个证明不仅仅是证明这一个例子。
假设一个人工智能提供了一个难以理解的、丑陋的证据。然后你就可以处理它，分析它。假设这个证明用了10个假设得到一个结论——如果我删除一个假设，这个证明还有效吗?这是一门目前还不存在的科学，因为我们还没有那么多人工智能生成的证明，但我认为会有一种新型的数学家，他们会利用人工智能生成的数学，让它变得更容易理解。比如，我们有理论科学和实验科学。有很多东西是我们凭经验发现的，但是我们做了更多的实验，我们发现了自然规律。我们现在在数学中不这么做。但我认为会有一个行业的人试图从最初没有任何洞察力的人工智能证据中提取洞察力。
那么，这不是数学的终结，而是数学的光明未来吗?
我认为会有不同的方法来做数学，只是现在还不存在。我可以看到项目经理数学家能够组织非常复杂的项目——他们并不理解所有的数学，但他们可以把事情分解成更小的部分，并把它们委派给其他人，他们有很好的人际交往能力。还有在子领域工作的专家。有些人擅长训练AI学习特定类型的数学，有些人可以将AI的证明转化为人类可读的东西。它将变得更像几乎所有其他现代工业的运作方式。比如，在新闻业，不是每个人都有相同的技能。有编辑，有记者，有商人，等等——我们最终会在数学领域有类似的东西。
我们所做的数学是与我们的大脑相匹配的，不是吗?如果在某一时刻人工智能变得如此聪明，它可能会进入我们难以理解的领域。
数学已经比任何一个人的头脑都要大。数学家通常依赖于其他人已经证明的结果。他们知道为什么它是对的，他们有一些直觉，但是他们不能把它分解成公理。但他们知道去哪里找，或者他们认识能找到的人。我们已经有了很多定理，这些定理只能通过计算机来验证，一些大规模的计算机计算已经检查了上百万种情况。你可以手工验证，但没人有时间这么做，也不值得。所以我认为我们会适应。一个人检查一切是没有必要的。让电脑帮我们检查，我觉得没问题。
在数学的前沿，有很多事情发生，把看似不相关的领域联系在一起，根据我天真的理解，一个了解所有这些领域的人工智能可以给你一个提示，说:“你为什么不看看那里?这也许能帮你解决问题。”
这是人工智能的一个非常令人兴奋的潜在用途，它可以创造联系，或者至少指出可能的联系。现在它的成功率非常低。它可能会给你10个建议，其中一个是有趣的，9个是垃圾。实际上，这几乎比随机还要糟糕。但这在未来可能会改变。
训练数学人工智能的道路上有什么问题?
部分问题在于它没有足够的数据来进行训练。网上有发表的论文，你可以在上面进行训练。但我认为很多直觉并不是在期刊上的印刷论文中捕捉到的，而是在与数学家的对话中，在讲座中，在我们给学生的建议中。有时我开玩笑说，我们需要做的是让GPT去接受标准的研究生教育，坐在研究生课上，像学生一样提问，像人类学习数学一样学习。
已发表的证明版本总是简明扼要的。即使你把人类历史上发表的所有数学数据都算进去，与这些模型训练的内容相比，它仍然很小。
人们只发表成功的故事。真正宝贵的数据来自于当某人尝试某件事时，它不太奏效，但他们知道如何解决它。但他们只发表成功的东西，而不是过程。
也许你应该努力证明些什么，比如医学研究。研究人员会注册它，然后即使它没有成功，他们也必须发表它。
我们没有那种文化。也许将来形式化会变得非常有效，你可以实时形式化。也许如果你想在一个研究项目中使用2040年的人工智能精益，你想获得使用这种人工智能的资金，你必须同意你尝试事物和失败的过程被记录下来。然后可以用来训练未来的人工智能。或者其他小组也在解决类似的问题，他们可以看到，“哦，另一个小组也做了同样的事情，但他们失败了，”这样你就不用浪费时间犯同样的错误了。
数学家是不是浪费了很多时间?
哦，非常喜欢。如此多的知识不知何故被困在数学家的头脑中。只有一小部分是明确的。但是我们形式化得越多，我们的隐性知识就会变得越明确。所以这会带来意想不到的好处。
这篇文章最初出现在《光谱》杂志上，并经许可转载。
