数学传统上是一门孤独的科学。1986年，安德鲁·怀尔斯隐居书房七年以证明费马大定理。由此产生的证明通常难以被同行理解，有些至今仍存在争议。但近年来，数学的越来越大领域已被严格分解为各自的组成部分（“形式化”），以至于证明可以由计算机检查和验证。
加州大学洛杉矶分校的陶哲轩坚信，这些方法为数学领域的合作开辟了全新的可能性。如果再加上人工智能的最新进展，未来几年该领域可能会建立全新的工作方式。借助计算机，大型未解决的问题可能会更接近解决。陶哲轩在接受《大众科学》德语姊妹刊物《Spektrum der Wissenschaft》采访时阐述了他对未来发展的看法。
[以下是经过编辑的采访记录。]
关于支持科学新闻
如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻报道 订阅。通过购买订阅，您将有助于确保有关塑造我们当今世界的发现和想法的具有影响力的故事的未来。
在您于旧金山举行的联合数学会议上的一次演讲中，您似乎暗示数学家彼此不信任。您是什么意思？
我的意思是，我们是信任的，但你必须亲自认识某人。除非你能逐行检查他们的工作，否则很难与从未见过面的人合作。通常最多[合作者]五个人。
随着自动化证明检查器的出现，这种情况正在发生怎样的变化？
现在你可以真正与数百名你从未见过的人合作。你不需要信任他们，因为他们上传代码，而Lean 编译器会验证它。你可以进行比我们通常做的更大规模的数学研究。当我形式化我们最近的成果，即所谓的 Polynomial Freiman-Ruzsa (PFR) 猜想时，[我与] 20 多人合作。我们将证明分解成许多小步骤，每个人都为一个小步骤贡献了一个证明。我不需要逐行检查贡献是否正确。我只需要对整个过程进行管理，并确保一切都朝着正确的方向发展。这是一种不同的数学研究方式，一种更现代的方式。
德国数学家和菲尔兹奖得主彼得·肖尔茨参与了一个 Lean 项目——尽管他告诉我他对计算机不太了解。
在这些形式化项目中，并非每个人都需要成为程序员。有些人可以只专注于数学方向；你只是将一个大型数学任务分解成许多较小的部分。然后有些人专门将这些较小的部分转化为形式证明。我们不需要每个人都成为程序员；我们只需要一些人成为程序员。这是一种劳动分工。
我大约在 20 年前就听说过机器辅助证明，当时这是一个非常理论的领域。每个人都认为你必须从头开始——形式化公理，然后进行基础几何或代数——而要达到更高的数学水平是超出人们想象的。是什么改变使得形式数学变得实用？
一个变化是标准数学库的开发。特别是 Lean，有一个名为 mathlib 的大型项目。本科数学的所有基本定理，例如微积分和拓扑学等等，都已被逐一放入这个库中。因此，人们已经努力从公理达到相当高的水平。梦想实际上是将[库]提升到研究生教育水平。那么形式化新的[数学]领域将容易得多。还有更好的搜索方法，因为如果你想证明某些东西，你必须能够找到已经确认是真实的东西。因此，真正智能的搜索引擎的开发也是一项重大的新发展。
所以这不是计算能力的问题？
不，一旦我们形式化了整个 PFR 项目，编译验证它只花了大约半个小时。这不是瓶颈——瓶颈在于让人类使用它，可用性，用户友好性。现在有数千人的大型社区，并且有一个非常活跃的在线论坛来讨论如何改进该语言。
Lean 是最先进的吗，还是有竞争系统？
Lean 可能是最活跃的社区。对于单作者项目，可能有一些其他语言略好，但 Lean 通常更容易上手。它有一个非常好的库和一个友好的社区。它最终可能会被替代品取代，但目前它是主要的正式语言。
当您谈论另一个数学项目时，有人问您是否想将其形式化，您基本上说这需要太长时间。
我可以形式化它，但这会占用我一个月的时间。目前我认为我们还没有达到常规性地形式化一切的程度。你必须精挑细选。你只想形式化那些真正对你有用的东西，例如教你如何在 Lean 中工作，或者如果其他人真的关心这个结果是否正确。但技术将会变得更好。所以我认为在许多情况下，更明智的做法是等待它变得更容易。而不是花费传统方式十倍的时间来形式化它，而是花费两倍的时间。
您甚至谈到将这个系数降到小于一。
借助人工智能，真正有可能做到这一点。我认为在未来，我们将不会再输入我们的证明，而是向一些 GPT 解释它们。GPT 会尝试在你进行时将其形式化为 Lean。如果一切都检查完毕，GPT 将[基本上]说，“这是你的 LaTeX 论文；这是你的 Lean 证明。如果你愿意，我可以按下这个按钮并为你将其提交给期刊。” 它在未来可能成为一个出色的助手。
到目前为止，证明的想法仍然必须来自人类数学家，不是吗？
是的，形式化最快的方法是首先找到人类证明。人类提出想法，证明的初稿。然后你将其转换为形式证明。将来，事情可能会以不同的方式进行。可能会有合作项目，我们不知道如何证明整个事情。但是人们对如何证明小部分有想法，他们将其形式化并尝试将它们组合在一起。将来，我可以想象一个大型定理由 20 个人和一群人工智能共同证明，每个人工智能都证明小东西。随着时间的推移，它们将被连接起来，你可以创造出一些美好的东西。那将是很棒的。在很多年之后才有可能实现。这项技术尚未成熟，部分原因是形式化现在非常痛苦。
我曾与一些人交谈过，他们尝试使用大型语言模型或类似的机器学习技术来创建新的证明。托尼·吴和克里斯蒂安·塞格迪最近与埃隆·马斯克等人共同创立了公司 xAI，他们告诉我，在两到三年内，数学将被“解决”，就像国际象棋被解决一样——机器在寻找证明方面将比任何人类都更出色。
我认为在三年内，人工智能将对数学家有用。它将成为一个伟大的副驾驶。你正在尝试证明一个定理，并且有一个步骤你认为它是真的，但你不太清楚它是如何成立的。你可以说，“人工智能，你能为我做这件事吗？” 它可能会说，“我想我可以证明这一点。” 我认为数学不会被解决。如果人工智能领域出现另一个重大突破，那是有可能的，但我要说的是，在三年内，你将看到显著的进步，并且实际使用人工智能将变得越来越容易。即使人工智能可以做我们现在所做的数学类型，这也意味着我们将转向更高类型的数学。所以现在，例如，我们一次证明一个定理。这就像个体工匠制作木偶或其他东西。你拿起一个木偶，非常仔细地绘制一切，等等，然后再拿起另一个。我们做数学的方式并没有太大改变。但是在每一种其他类型的学科中，我们都有大规模生产。因此，借助人工智能，我们可以开始一次证明数百个或数千个定理。人类数学家将指导人工智能执行各种操作。所以我认为我们做数学的方式会改变，但他们的时间框架可能有点激进。
我在 2018 年彼得·肖尔茨获得菲尔兹奖时采访了他。我问他，有多少人理解你在做什么？他说大约有 10 个人。
通过形式化项目，我们注意到的是，你可以与不了解整个项目数学的人合作，但他们了解其中很小的一部分。这就像任何现代设备一样。没有人能够独自制造一台计算机，开采所有金属并提炼它们，然后创建硬件和软件。我们有所有这些专家，我们有一个庞大的物流供应链，最终我们可以制造智能手机或其他东西。目前，在数学合作中，每个人都必须几乎了解所有的数学，正如 [肖尔茨] 提到的那样，这是一个绊脚石。但是通过这些形式化，可以将项目分门别类，并且只需了解项目的一部分即可做出贡献。我认为我们也应该开始形式化教科书。如果教科书被形式化，你可以创建这些非常互动的教科书，你可以在非常高的层次上描述结果的证明，假设有很多知识。但是，如果有一些步骤你不理解，你可以展开它们并深入细节——如果你愿意，可以一直追溯到公理。目前没有人为教科书这样做，因为工作量太大了。但是，如果你已经将其形式化，计算机可以为你创建这些互动的教科书。这将使一个领域的数学家更容易开始为另一个领域做出贡献，因为你可以精确地指定一个大型任务的子任务，而这些子任务不需要理解一切。
数学证明不仅仅是检查某件事是否正确。证明也是为了理解某些东西，对吗？有美丽的证明，也有非常技术性的丑陋证明。一个好的证明能让你对问题有更高的理解。因此，如果我们将其委托给机器，我们还能理解它们发现了什么吗？
数学家正在做的是，我们正在探索什么是真，什么是假，以及为什么事情是真的。我们这样做的方式是通过证明。每个人都知道，当它是真的时，我们必须尝试证明它或证伪它。这需要很多时间。这很乏味。但在未来，也许我们只会问人工智能，“这是真的还是假的？” 我们可以更有效地探索空间，我们可以尝试专注于我们真正关心的东西。人工智能将通过加速这个过程为我们提供很大帮助。至少目前，我们仍将是驾驶员。也许 50 年后情况会有所不同。但在短期内，人工智能将首先自动化那些枯燥、琐碎的事情。
人工智能会帮助我们解决数学中尚未解决的重大问题吗？
如果你想证明一个尚未解决的猜想，你需要做的第一件事就是将其分解成更小的部分，每个部分都有更大的可能被证明。但是你经常会将一个问题分解成更难的问题。将一个问题转化为比它更难的问题很容易，但转化为比它更简单的问题则很难。人工智能尚未表现出在这方面比人类更好的能力。
通过分解问题并进行探索，你也会在此过程中学到很多新东西。例如，费马大定理是一个关于自然数的简单猜想，但为证明它而开发的数学不再仅仅是关于自然数的了。因此，解决一个证明远不止证明这一个实例。
假设人工智能提供了一个难以理解、丑陋的证明。那么你可以与它合作，你可以分析它。假设这个证明使用 10 个假设来得到一个结论——如果我删除一个假设，证明仍然有效吗？这是一门尚不存在的科学，因为我们没有那么多人工智能生成的证明，但我认为未来会出现一种新型的数学家，他们将采用人工智能生成的数学，并使其更易于理解。就像我们有理论科学和实验科学一样。我们通过经验发现了很多东西，然后我们做更多的实验，我们发现了自然规律。我们现在在数学中没有这样做。但我认为会有一个行业的人试图从最初没有任何见解的人工智能证明中提取见解。
因此，这不会是数学的终结，而是数学的光明未来吗？
我认为未来会出现现在根本不存在的不同数学研究方式。我可以看到项目经理数学家，他们可以组织非常复杂的项目——他们不理解所有的数学，但他们可以将事情分解成更小的部分并委托给其他人，并且他们具有良好的人际交往能力。然后是有在子领域工作的专家。有些人擅长训练人工智能进行特定类型的数学，还有些人可以将人工智能证明转化为人类可读的东西。它将变得更像几乎任何其他现代产业的运作方式。例如，在新闻业中，并非每个人都具备相同的技能。你有编辑、记者和商人等等——我们最终会在数学中拥有类似的东西。
我们所做的数学是与我们的大脑相匹配的数学，不是吗？如果人工智能在某些时候变得如此聪明，它可能会进入我们难以理解的领域。
数学已经比任何一个人类头脑都要大了。数学家通常依赖其他人已经证明的结果。他们有点知道为什么它是真的，他们有一些直觉，但他们无法将其完全分解到公理。但他们知道在哪里寻找，或者也许他们认识可以做到的人。我们已经有很多定理只通过计算机验证，其中一些大规模计算机计算已经检查了一百万个案例。你可以手工验证它，但没有人有时间去做，而且不值得。所以我认为我们会适应的。一个人不必检查一切。让计算机为我们做检查，这对我来说很好。
在数学前沿，正在发生很多事情，这些事情将看似无关的领域结合在一起，根据我的天真理解，一个了解所有这些领域的人工智能可以给你一个提示，说：“你为什么不看看那里？那可能会帮助你解决你的问题。”
人工智能的一个非常令人兴奋的潜在用途是创建联系，或者至少指出可能的联系。目前，它的成功率非常低。它可能会给你 10 个建议，其中一个是有趣的，九个是垃圾。实际上，它几乎比随机的还要糟糕。但这在未来可能会改变。
训练数学人工智能的障碍是什么？
部分问题在于它没有足够的数据进行训练。网上有已发表的论文，你可以用它们来训练它。但我认为，很多直觉并没有体现在期刊上发表的论文中，而是体现在与数学家的对话中，体现在讲座中以及我们指导学生的方式中。有时我开玩笑说，我们需要做的是让 GPT 接受标准的毕业教育，坐在研究生课堂上，像学生一样提问，像人类学习数学一样学习。
证明的已发表版本总是经过压缩的。即使你收集了人类历史上所有已发表的数学成果，与这些模型所训练的数据相比，仍然很少。
人们只发表成功的故事。真正珍贵的数据来自某人尝试做某事，但它不太奏效，但他们知道如何修复它。但他们只发表成功的事情，而不是过程。
也许你应该像医学研究那样，注册努力证明某件事。研究人员会注册它，然后即使它没有成功，他们也必须发表它。
我们没有那种文化。也许在未来，形式化将变得非常高效，你也许能够实时形式化事物。也许如果你想在研究项目中使用 2040 年一些花哨的人工智能 Lean，并且你想获得资金来使用这个花哨的人工智能，你必须同意记录你尝试和失败的过程。然后，这可以用来训练未来的人工智能。或者，也许其他一些小组正在研究类似的问题，他们可以看到，“哦，另一个小组尝试了同样的事情，但他们失败了”，这样你就不会浪费时间犯完全相同的错误。
数学家是否浪费了很多时间？
哦，非常浪费。如此多的知识不知何故被困在个体数学家的头脑中。只有一小部分被明确化。但是，我们越形式化，我们更多的隐性知识就会变得显性。因此，这将带来意想不到的好处。
本文最初发表于《Spektrum der Wissenschaft》，经许可转载。