Transcription
各位听众，大家好，欢迎来到 No Priors。今天我们请到了 DeepMind AlphaProof 团队的 Thomas Hubert、Rishi Meta 和 Laurence Saran。AlphaProof 是一个新的人工智能系统，能够寻找和验证数学证明，它建立在 DeepMind 在国际象棋和围棋领域早期成功的基础上，旨在应对人工智能领域最严峻的挑战之一：数学推理。在本期节目中，我们将探讨 AlphaProof 的工作原理、它对数学和人工智能的意义，以及关于测试时强化学习（test time RL）的更多信息，并揭示它对机器学习进行严谨推理的能力有何启示。非常高兴能邀请到各位，欢迎你们！
谢谢你们的邀请。
是的，也许你们可以先简单介绍一下你们各自的背景，以及你们是如何一起开始研究 AlphaProof 的。
我是 Rishi，我是 AlphaProof 的技术负责人之一。我从事计算机科学和机器学习领域已经有一段时间了。我是一名国际象棋玩家，我偶然看到了 AlphaZero 的论文，并看到了一些那个智能体产生的国际象棋对局。我觉得这非常鼓舞人心，我想，这就是我需要从事的事业，创造出一些优美、超人类、甚至近乎异类的东西，这感觉就像魔法一样。
我来到 DeepMind，而 Thomas 领导的 AlphaZero 团队正在研究数学，这就是我如何进入数学领域的。
我的背景是这样的，是的，在我职业生涯早期，我曾在工业界工作。我研究过计算机网络检测，研究过广告定位，然后转到了人工智能研究。我一直对能够投入更多计算资源来解决难题或进行更深入思考的系统感兴趣，而数学似乎是实现这一目标的完美领域。
就我而言，我实际上是一名围棋玩家。所以，从 10 岁开始，我不是在编程，而是在下围棋，我在年轻时下了很多围棋。然后，在某个时候，这也是我父亲的梦想，想开发一个计算机围棋程序。所以我一直在思考，我需要了解什么才能成为那个计算机围棋程序？然后我意识到，也许当时它正在被开发。这就是我发现 DeepMind 的方式，以及我如何发现通用人工智能（AGI）的，也是我加入这家公司的方式。我一直参与 AlphaGo、AlphaZero 以及这一系列工作。最近，我们还研究了 AlphaCode 和 AlphaTensor。所以，你知道，这比国际象棋早得多，但我们已经知道 Transformer 正在一点点改变事物运作的方式。所以，我们发现，在数学领域，你可以获得完美的验证性，而通过 AlphaCode，我们意识到我们可以生成很多好的代码。因此，当时考虑数学的潜力是非常自然的。
你能对比一下……嗯，也许作为背景介绍，对于像我这样不是超级运动员的听众来说，国际数学奥林匹克（IMO）是……可以说是最古老、最负盛名的青少年数学竞赛。有一系列六个问题，它们被认为是极其困难的，而 AlphaProof 在今年解决了其中的四个问题，取得了非常惊人的成果。你能谈谈……嗯……特别是 IMO 中的数学问题，与下棋和其他搜索问题（如国际象棋）相比，它是一个什么样的问题吗？
我认为，首先，有一个很大的区别，那就是棋盘游戏是……你是和别人对弈，这很有趣。在棋盘游戏中，例如，当我们开发 AlphaGo、AlphaZero 算法时，我们可以真正实现……自我对弈。你可以一直与一个和你实力相当的对手对弈，而这被证明是一个强大的想法。在某种意义上，当你试图学习数学时，你并没有真正的对手。你只需要思考它。数学有点特别，因为它几乎是一种纯粹的认知活动，你只能……你唯一能做的就是更深入地思考。你知道，你可能无法真正进入现实世界进行实验。我猜数学家们说，有时候打个盹是个好主意，你的潜意识会思考这个问题，这是产生新想法的好方法。但它很大程度上是关于思考的。所以，你知道，当你面对一个真正困难的问题时，如何去尝试解决它，这是一个很大的问题。
也许现在是时候请你向我们的听众——他们大多数是技术人员或在科技领域工作的人，但也包括更广泛的商业受众——描述一下，AlphaProof 的整体架构是如何工作的？
好的，当然。AlphaProof 基于一种叫做 AlphaZero 的东西。所以，也许我先从那里开始。AlphaZero 是我们开发的一个程序，它基本上可以……处理信息完美的棋盘游戏。它的工作原理也基于一种强化学习算法。所以，你可以把 AlphaZero 看作是三个组成部分：第一，一个神经网络；第二，大规模强化学习，基本上是从试错中学习；第三，它还有一个规划和搜索的组成部分，试图在当前情况下寻找……最佳答案。
结果是，你知道，也许我们当时在下棋时并没有想到这一点，但如果你能处理……无限的行动空间，那么，你知道，与其寻找一个棋步，你可以寻找……例如，一个证明的思路。这就是我们在开始 AlphaProof 时所做的尝试：我们能否……我们的行动空间是生成证明的思路。而且，也许非常重要的是，我们为此使用了形式化语言。所以，基本上，换句话说，我们使用代码来写数学。这最近变得相当流行。它的优点是，一旦……证明完成，你的……你知道，机器会给你一个信号，告诉你，是的，你的证明是正确的，或者不是。所以，我们可以搜索……正确的证明。一旦我们找到一个正确的证明，我们就可以从中学习，并获得一个更好的神经网络，然后进入这种自我改进的循环，处理越来越难的问题，并越来越多地了解数学。所以，总的来说，这就是它的工作原理，以及 AlphaZero 的思想是如何应用于数学的。
你宣布时提到的一件有趣的事情是，有一系列问题，有些问题几分钟就解决了，有些问题需要三天来解决。你能描述一下数学的整体搜索空间，或者 AlphaProof 在哪些领域更擅长，哪些领域相对较弱吗？比如数学中的推理类型？
数学的搜索空间比国际象棋或其他棋盘游戏要大得多。所以，你知道，有些人可能认为写数学证明就像每一步都从一个已知技巧的袋子里 picking。但实际上，有很多证明需要……你必须想出一些非试探性的构造。你必须凭空发明一个函数，或者你必须……想出一种方法来操作，即使你只是重写一个表达式，你也可以用无限种方式重写它，而只有少数几种方式可以真正推进证明。有时，思考一个新颖的问题需要……几十年的理论构建，并从一个全新的角度来处理它，才能得出有助于解决问题的角度。所以，在这种意义上，你知道，有很多数学问题，它们陈述起来很简单，但却经受住了时间的考验，因为它们几个世纪以来一直未解决，就是因为……在大多数情况下，搜索空间并不容易导航。
我认为 AlphaProof 在 IMO 的类别中表现出色的是，它在……它在代数和数论方面表现得相当好。它在组合数学方面相对较弱，尽管它在某些 IMO 组合数学问题上表现相当不错。而且，我们在今年的比赛中没有将其应用于几何学。它导航这个巨大的搜索空间的一种方式是通过一个我们想出的叫做测试时强化学习（test time RL）的想法。这是一个这样的想法：假设你面临一个你不知道如何解决的问题，你知道你可以用你现在所知道的进行一些搜索，但你找不到证明。那么，智能体就会……它会构造这个问题的许多变体，并尝试解决所有这些问题。如果它设法解决了其中任何一个，它就会从这次经历中学习，并……越来越接近解决原始问题。你可以把它想象成……当你面对一个新的科学问题时，你从其他问题中获得的许多先验知识可能不直接适用于它。相反，你必须对这个问题本身进行非常定制化的实验来学习它，然后才能……逐步走向解决这个问题。所以，这个过程模仿了这一点。所以，当你谈论……那些需要三天才能解决的问题时，这些就是那些……我们无法用基础网络解决的问题，但我们提出了许多许多变体，我们尝试了所有这些变体，一点一点地改进，然后……经过几天的计算时间，我们才找到了最终的解决方案。
关于 AlphaProof 的局限性或扩展其可解决问题集的方法有哪些？我猜这有两个方面。一方面，它已经做得相当好的领域，比如代数和其他领域。另一方面，有些领域可能需要新的训练数据或其他东西，比如几何学的某些方面，或者其他……数学领域。我有点好奇，你认为要从现在开始显著提高性能需要什么？显然，你们所做的非常令人印象深刻。我只是好奇，你们是如何看待未来增长的障碍的？
也许 AlphaProof 主要不做的就是……理论构建。它不产生理论。AlphaProof 和……装备齐全的数论，将无法得出……推导数论结果所需的复杂分析。所以，这是我们不……甚至不生成变体并从中学习以解决我们感兴趣的原始问题的主要事情之一。理论构建是一个……一个需要进一步发展的组成部分。
另一个方面是，有些问题，比如组合数学，可以……以一种有点晦涩的方式陈述。这并不意味着所有组合数学问题……就像……组合数学问题都与计算事物的数量有关。例如，如果你有一个袜子收纳器里有 40 只袜子，你有多少双？它们可以以某种晦涩的方式陈述，如何……将它们翻译过来是一个主要的困难，然后如何解决它们。这个问题有点……有点棘手。如何最好地解决它仍然是一个悬而未决的问题。但我认为这与你的理论构建有点联系，因为例如，你知道，困难的一部分来自于……表达这些事物所需的工具目前并不存在于我们正在使用的库中。所以，例如，如果你有一些……表达……什么是智能体，什么是环境，什么是策略的东西，那么，例如，大多数……很多组合数学问题就会更容易陈述。但因为目前不存在，所以……某种意义上，自动形式化需要……在实际形式化问题之前，先想出所有这些东西。所以，这可能与……你知道，在某个时候，你需要能够开发新的定义、新的数学对象，然后想出它们的性质和证明等等。
我猜，我想是 1900 年，大卫·希尔伯特提出了他著名的 23 个问题，这些问题在当时定义了许多他认为对数学很重要的领域，以及那些重要的、热门的未解决问题。或者，我猜，作为一个普遍的问题，是否存在某种图灵测试的等价物？
这是一个非常好的问题。它……它完全定义了……你知道，20 世纪的数学，也许……千禧年问题……你知道，七个千禧年问题，其中只有一个已经解决。这是另一个尝试定义……你知道，21 世纪数学可能的发展轨迹。我们解决这些问题的机会有多大？这是一个……这是一个非常困难的问题，因为我们知道……你知道，我们的大脑是线性思考的，但我们从经验和研究人工智能中知道，我们实际上应该尝试指数级思考。事情可能会很快发生变化。同时，你知道，我认为我们不知道……像黎曼猜想这样的东西有多难。它是……它是比我们现在能做的……低两个数量级，三个数量级，也许是十个数量级？因为我们没有……存在性的证明。很难……很难估计它到底有多难。但我认为，解决这个问题将涉及……创造全新的数学、全新的理论等等。所以，如果我们想让 AlphaProof 达到那个水平，我认为我们需要……要么它会自然出现，这是可能的，因为……你知道，要证明更难的问题，你开始需要能够引入这种新的……数学对象……来分解问题。我们在 IMO 上已经看到了这一点，虽然规模很小，但很有可能它会仅仅通过尝试解决问题而出现，或者，你知道，我们必须……更明确地思考构建理论意味着什么，以及我们如何鼓励 AI 来做这些事情。
只是为了……我们的听众朋友们，他们不像我一样花那么多时间在未解决的数学问题上……只是为了稍微解释一下，黎曼猜想基本上预测……素数遵循一个特定的模式，比如分布。它具有重要的意义。也许我们可以从那里开始，思考一下……当你们开始将数学作为搜索空间进行研究时……有很多有趣的假设……比如为什么要去研究数学？一种是……这个领域本身。所以，我想知道你们是否有……想研究的问题。另一种是……这种推理能力的进步将使我们能够……它将转移到其他领域，无论是……科学，还是我们认为更……基于语言的、可验证性较低的、非代码、非基于规则的领域。你们想把这个带到哪里去？
我不是一个真正的数学家，所以我没有……我没有一个绝对想解决的问题。但它一直是我学生时代最喜欢的科目。而且，我认为你是绝对正确的。有……你知道，至少有两种……主要的原因，为什么你可能想花很多时间在数学上。一个是……我认为它被描述为……宇宙的语言。你知道，它在描述和预测自然世界以及塑造它方面都非常强大。而且，你看到……基本上，我们看到数学是……我们现在使用的所有技术的核心。所以，对数学有很好的理解，可能……非常重要，以理解我们当今的世界。然后，当然，你可以……正如你所暗示的，争辩说……你知道，解决数学问题，或者……这需要……推理、泛化、抽象，所有这些我们谈论……像认知人工智能这样的东西时所考虑的东西……将是……将是……是通往……人工智能的道路，这可以真正帮助……人工智能的发展。所以，我认为，至少对我来说……你知道，这些可能是……为什么数学是一个特别有趣的话题，值得去普遍解决的两个主要原因，尽管……你知道，数学，好吧，让我们说它仍然是一个……受限的领域，但它具有……无限的复杂性，而且它确实代表了很多东西。但它可能值得……集中精力去做，因为它可能带来的所有潜在影响。
我可以……这是关于我的动机。我一直对……创造能够通过更深入思考而变得更好的系统的问题感兴趣。我在机器翻译、文本扩散和导航智能体中看到了这一点，这些智能体通过更深入的思考来发现环境。数学似乎尤其……证明陈述。AlphaProof 的核心……似乎是最后一个主要的挑战领域，我还有很长的路要走。而……一个关键的要素将是找到一种……更深入的思考方式，这种思考方式可以表现为更多的搜索，可以是测试时强化学习，也许下一步的更深入思考……将是如此深入的思考，以至于智能体能够提出自己的理论。所以，数学……就像思考更多的技巧一样。
我的动机是什么？追求人工智能的根本原因之一是……揭示宇宙的秘密。你知道，关于……为什么事物会以这种方式运作，我们为什么在这里，以及……为什么我会有意识，以及发生了什么。我猜，数学……解决这些纯粹的数学问题，感觉就像……我们已经……有很多人正在这样做。他们将数学视为对真理的追求。你知道，人们研究这些问题，不是因为它们有任何应用，而是因为……你知道，到底答案是什么？为什么这个东西会这样运作？解决黎曼猜想这样的事情，感觉就像……它具有……一种纯粹的对真理的追求的风格，这很有吸引力。
我猜，与此相关的是……你知道，在数学中，或者……在科学中，或者科学和数学中……有一个悠久的传统，人们……为了它们本身而做事，或者为了知识的追求而做事。而且，你知道，Sarah 提到了一个例子，数论及其在密码学中的应用，零知识证明在加密货币中以不同的方式出现。你知道……群论和代数随着时间的推移在量子力学中得到了发展，并且……事先被开发出来，然后又得到了进一步的发展。你对……你正在做的一些工作的应用领域有什么特别兴奋的吗？还是主要是……为了理论部分的乐趣而做的？
这是一个好问题。我认为我们可以……也许答案取决于我们每个人。我认为有一件事让我很受鼓舞，那就是向数学家学习……他们对什么感兴趣，以及他们在当前……数学世界中发现什么有趣。所以，例如，你知道，我一直在读一本叫做……兰兰兹纲领的东西，它试图连接……数学的不同领域。它被描述为……就像在物理学中，你试图寻找……统一的物理学理论一样，它试图寻找……统一的数学理论，也许……你知道，我们有数论在这里，我们有……几何学在那里，但也许……有什么东西……更具统一性。所以，我个人喜欢那些抽象的想法，即使我可能不太理解它们。但是，是的，我非常愿意……看看……数学家们关心什么，而且他们之间可能也会有分歧。
是的，我认为他们会有分歧。如果你看看历史上的例子，比如当 Bombelli 开始研究虚数时，他被……我不知道，当时更重要的数学家们完全嘲笑了。很多年后，我们得到了交流电和描述电的能力。所以，我认为这是一个……一个非常有趣的问题，如果……如果你有机器，机器能够开发自己的定理，你把它指向哪里才能找到兴趣或最终的用处，这是一个非常大的问题。
有一个领域我特别兴奋，那就是……代码验证。目前，当我们编写软件时，我们……编写代码并编写测试。当测试通过时，我们相当满意。偶尔会出现……通过测试的错误，甚至安全问题。如果我们可以用代码表达算法应该验证的属性，并在代码中证明……算法确实验证了这些属性，那会好得多。这已经在非常关键的领域，比如航空电子学和密码学中完成了，在那里它非常重要。我认为，如果……验证更加普遍，并且如果我们消除了瓶颈……也就是人类编写这些证明，那么软件行业将会处于一个更好的状态。如果人类能够得到……专门工具的支持，我们就能处理……大量的证明，我认为这将是向前迈出的一大步。
另一个我感到兴奋的应用领域是……这项技术向许多其他领域的转移。所以，你知道，有两种……两种参与者。一种是……数学推理技能的转移，这个智能体通过这种训练获得的技能，转移到许多其他领域。而且，你知道，正如我们所见，数学对于工程和科学至关重要，等等。但是，你知道，我们在这里开发的一些技术，比如……扩展强化学习，以及……弄清楚如何花费大量的推理时间计算等等，感觉它适用于许多其他问题。
我要问一个……一个更具推测性的问题。我们一直在谈论数学和代码，以及……那些不容易形式化但可以形式化和验证的领域。你认为这在语言领域有多大的适用性？例如，一个智能体能否让某件事变得更有趣？而且，判断某件事是否有趣比……写一个好的单口喜剧表演要容易得多，对吧？所以，我认为这是一个……一个有启发性的例子。但是，你对……如何……从……验证正确性或质量的能力中吸取一些经验教训……在强化学习方法中，有什么直觉吗？
嗯，正如你所说，你知道，有些领域存在……地面真实性，有些领域则不存在。所以，当不存在时，你知道，比如……有趣可能是一种……你知道，一种人类……一种模糊的人类概念，也许那里有……外星人，他们会有不同的幽默感。所以，对于那些……那种问题，我认为……你获得……你的基础的唯一方法是通过……人类是你的基础。对于其他领域，也许……现实世界是某种基础，然后……你知道，你必须去现实世界来获得你的基础。但是，基本上，你知道……强化学习可以让你说，好吧，你知道……我的奖励来自哪里？我猜有时它来自……现实世界，有时你可以完美地计算它，有时……你知道，奖励来自人类。而且，我认为这很好。
基本上，有一些技术……我们开发了，你知道，当然，当你能够……机器检查事物时，你可以……以一种……与……如果你必须问人类相比，非常不同的规模运行。总的来说，即使我们是……我们是很多人，所以仍然可能有很多……扩展的可能性，特别是对于像这样的事情，你知道……比如幽默……每个人都应该……对什么是有趣的或不是的发表意见。所以，绝对，你知道，例如，强化学习框架……我认为仍然是一个很好的框架来思考这些问题。而且，你知道，是什么让强化学习起作用的一部分，也应该……转移。也许我们依赖于……形式化验证的东西，也许它不会转移到那个特定的……
在那些更可验证的领域，人类的评分或输入，比如……明确描述或标记他们的推理，还有空间吗？比如，如果你可以无限地访问定理证明器来为你进行标记，那有用吗？或者……你应该如何看待它，而不是……只是进行更多的搜索，并致力于更好的形式化？
AlphaProof 的运作方式是，它自己发现证明，当它们有效时，它会从中学习并发展出自己的风格，这被评论为……看起来确实……相当异类。如果无限访问定理证明器，它会创建……正确的证明，并带有某种……人类的……特殊性。我们可以开始在……证明的集合中进行优化，以获得看起来……对解释性有用的证明，用于教学目的。所以，在这个……有效证明的空间中，肯定还有……对人类可能更喜欢的证明的空间。
这在某种程度上是一个非常严厉的声明，不是吗？因为它……它只是……偏好，而不是……也许……能力进步。如果证明看起来很异类，我……我会在乎吗？如果……我们拥有知识，解释性在这种情况下似乎很有用。是的，是的，我说的就是……这肯定不是唯一的角度。
有了更多的监督数据，我们可以避免探索问题，我们可以……翻译所有已知的……人类的证明，这肯定会使智能体变得更好，而且肯定会为我们节省多年的计算时间。我并不是说解释性是唯一的方式。过渡肯定可以。但它可能会提供我们无法获得的信号。
假设，随着时间的推移和计算能力的提高，我们可能会……重新发现已有的证明。我认为这是一个有趣的问题，因为它……它突出了……专业人类数据和……强化学习数据的互补性。而且，我认为这在……大型语言模型中尤其突出，因为……大型语言模型产生了……它们具有非常强大的人类先验知识，因为它们在大量人类数据上进行了预训练。但是，当我们……用它们进行强化学习时，它们有机会……利用这些人类先验知识，并在它们的基础上发展出自己的……做事风格，就像 AlphaProof 所做的那样。我认为我们在这个项目中看到的一件事是，通常……少量的宝贵人类数据可以……非常有用，可以……为智能体播下行为的种子，并……让它从一个完全零的状态……到一个……高得多的水平，在那里它可以……以更有效的方式与环境互动。然后，它可以在此基础上进一步发展，并且……也许匹配或超越人类，但以自己的风格。这就是……我认为……这可能是未来大型语言模型强化学习的方式。专业人类将……帮助大型语言模型从……一堆知道如何做任何事情的权重……到一个……令人惊讶地强大的东西，然后强化学习将从那里开始，将其提升到……超人类的水平。
我想是庞加莱，有人说他是最后一个知道所有数学的数学家，或者至少……理解了大部分数学。突然之间，你就有了一个人工智能或一个系统，它有可能在一个程序中封装所有的数学。它可以真正用作……检查证明的工具，它可以帮助……推动数学家在自己的研究中前进。你知道，现在有人证明了某件事，如果他们在更小的领域，能够真正验证或检查他们所做证明的人并不多。
有多少数学家现在可以使用 AlphaProof？你如何看待与数学界就这项非常了不起的……一系列进展的日常使用进行互动？
目前，你知道，数学家们无法使用 AlphaProof。说实话，你知道，就像……我们目前完全无法与……像定理证明器这样的人相提并论。我认为我们……我们所证明的是，我们能够……几乎从零开始学习通用数学，并达到……令人印象深刻的高中水平。然后，我们需要……增长我们的知识库，以便我们变得有用。
我不知道你是否看到过……特伦斯·陶近期的采访，在过去一年里。他一直在说，你知道，数学中一个有趣的事情是，合作相对较少。很多论文都是一两篇作者的论文，最多五篇。这是因为……与更多的数学家合作非常困难，因为你需要检查他们正在做什么。而且，这非常耗时。但如果你取而代之的是依赖于一个形式化系统来检查其他人的工作，那么你就可以……有点像天文学，你可以有一个业余爱好者……住在……中间，住在任何地方，你从未见过他，然后你就不必信任他了。你可以……在某种意义上信任……机器来检查工作。如果机器说这是一个……正确的证明，那么它就是一个正确的证明。然后你就可以开始与……更多的人合作。在某种意义上，这很酷，因为……你可以开始考虑……在许多人类之间进行合作，也可能……人工智能之间。所以，这可能是……这也是我们思考它的方式之一。哦，我们能否……我们能否潜在地合作进行这些项目？
目前，我们认为……我们更多地将自己视为……如果能成为一名研究生，那就太好了。数学家们可以给我们……问题。我认为这可能……与理论构建有关。目前，我们非常擅长提出正确的问题。而且，绝对……我们希望依靠……整个数学界来……提出他们关心的问题，看看我们是否能……即使是一点点地帮助回答这些问题。
我小时候也是一名围棋玩家。所以……你知道，看到……最不寻常的数学，以及……正如你所描述的，围棋中的异类走法，对我来说也非常有趣。到目前为止，AlphaProof 的证明中有什么让你觉得异类或令人惊讶的吗？你能谈谈吗？
是的，当然。让我给你们……展示一下 AlphaProof 为今年 IMO 的……第六题提出的证明，或者证明的一部分。我认为如果我把它显示在屏幕上，会更容易理解。
所以，这是第六题。IMO 通常有六个问题。问题三和六是最难的。所以，这被认为是今年 IMO 最难的问题之一，但实际上它是有史以来最难的问题之一，因为……在 500 多名参赛者中，只有五人设法解决了它。所以，你知道，它确实非常难。所以，我们可以非常快速地回顾一下这个问题在说什么，我不会详细介绍整个证明，因为在我们有时间的情况下，它可能难以理解。但我会……指出一个…… AlphaProof 提出的很酷的构造。
问题讨论了一个函数的定义，该函数被称为“Aquasuyan”。Aquasuyan 并不是一个真正的数学术语，这只是一个俏皮的说法，指的是……比赛举办地巴斯……罗马人曾经称之为 Aquasulis。但无论如何，他们给了我们两个方程来表征一个 Aquasuyan 函数。我们必须证明……存在一些整数 C，使得对于任何 Aquasuyan 函数 f，这种形式的……有理数最多有 C 个不同的值。
这有点复杂，但基本上，这种形式是……函数的一个“偶数部分”。它试图说明的是，你知道，你可以……取任何 Aquasuyan 函数，给它很多有理数，然后……计算这个表达式对于很多有理数的值，你可能会得到无限个值，或者你可能会得到五个值，三个值。所以，它要求你证明存在一个界限 C，你不能有超过 C 个唯一值。它还要求你找出这个界限 C 是什么。
所以，经常……好的，这就是问题。C 是什么？所以，经常当你试图回答这样的问题时，一个策略是……显示 C 的上限和下限，然后显示这两个收敛，然后你就找到了 C。
我将从 AlphaProof 已经证明 C 小于或等于 2 的地方开始。这本身就是一个非常有趣的证明，如果你有兴趣，可以在我们的博客文章中查看。但在这个证明的这一点，AlphaProof 必须决定 C 是 1 还是 2。它将不得不通过……找到……来决定。所以，很容易证明 C 可以是 1。难的是……是否存在任何 Aquasuyan 函数 f，使得 C 是 2？你知道，你可以暂停并尝试……找到遵循这些……这些……属性的函数 f，并……看看你是否能找到一个，对于它，你可以找到这个 F(r) + F(-r) 表达式的两个不同的值。
但有趣的是，Tim Gowers，他是我们的评委之一，也是一位菲尔兹奖得主，他花了几个小时尝试这个问题，但他找不到……具有这种属性的函数的构造。当然，这并不是说 AlphaProof 在数学上比 Tim Gowers 更好，这只是突显了这个问题这一部分的难度。而 AlphaProof 提出了……这个构造，即函数 f(x) = -x + 2 * ceil(x)。这是一个看起来很奇怪的函数，我在这里绘制了它。有趣的是，这个函数……如果你代入 r = -1 和 r = 1/2，你会得到两个不同的值。所以，你可以知道 C 必须等于 2。
在我看来，这可能是 AlphaProof 解决过的最难的问题。这是一个非常酷的、奇怪的构造，它依赖于这种……这种 ceiling 函数。非常酷，非常酷。
我们可以从给今天从事数学研究并投入时间的人的建议开始吗？考虑到 AlphaProof 和相关的模型，形式化数学将变得越来越重要，不仅因为……人工智能将成为形式化数学中一个非常强大的工具，而且因为它……正在成为数学家之间合作的一种方式，许多杰出的数学家正在采用它。而且，你知道，在数学界，仍然只有少数人使用 Lean，但……这是一个不断增长的少数群体。而……人工智能只会加速这一点。所以，我想，我不是数学家，我怎么能给数学家建议呢？但我想，我从外部的建议是……尽早学习 Lean。我也意识到，它是一个很好的教育工具，因为……你知道，大多数证明都是以……写证明的人的抽象水平来编写的。所以，例如，你知道，如果那个人认为这一步是……微不足道的，那么，你知道，你不会得到任何解释。但如果你有……用形式化语言写的证明，你就可以……放大到……适合你的细节水平。所以，这是你可以……按照自己的水平学到更多的东西。第二件事是……你实际上可以……在某种意义上与自己进行自我对弈。你知道，也许你正在学习……数学的一个非常抽象的部分，而这……通常的事情是……解释数学很难，因为它……相当抽象，然后你可能无法判断你所做的是否正确。而且，如果你在纸上做，那么，也许你能做的最好的事情就是……找人或你的老师，这可能需要很多时间才能得到反馈。但如果你使用的是形式化语言，那么，你知道，你就会确切地知道……如果你做得正确，或者你……有点欺骗了自己，还有什么需要证明的。所以，即使是为了教育目的，我认为它可能非常有趣。
这不是建议，而是……值得推测。我……有人说有两种数学家：一种是构建理论的，另一种是……证明定理的。我理解，为了证明定理，有时你必须……构建整个理论，就像……对于 AlphaProof 所做的那样。但似乎……在构建理论方面，比在证明定理方面，有更多的空间留给……人类的创造力、人类的品味、人类的技能。
我在这里有点挣扎的一件事是，在许多……正在被……人工智能所攀登的领域，品味似乎越来越重要。这可能是……在算术级数素数周围的问题，因为它实际上会导致……方法和工具的进步。但我实际上认为，这是一个……这是一个挑战，因为……告诉某人“培养良好的品味”是一个……比“确保你学习 Lean”更微妙的指令。但二，它也很有趣，并且与你们所做的工作平行，因为……在某种程度上，你知道，如果你看看你应用计算的行为，就像……哦，好吧，当你处理……抽象地处理……这个领域周围的一些问题时，你会认为……这将提高你解决问题的能力。所以，我认为，也许正如你所说，好吧，我们将进行更多的测试时强化学习。我不知道我们是否都会培养品味，即使它看起来很有用。
我从某个地方看到了这个：随着机器在寻找答案方面变得越来越好，我们将不得不擅长寻找问题。而且，你知道，这些系统没有……它们自己的……关于什么问题是有趣的，以及给定一个大问题，我如何将其分解成可能有趣的小问题。而且，你知道，这可能就是……不仅在数学中，而且在许多领域，即使作为……软件工程师，我也发现我的工作越来越多地不是解决……低级细节，而是……做出好的高层决策，工具可以帮助你。而且，我认为这对于越来越多的人来说将是真实的。
非常感谢你们。很高兴见到你们所有人，感谢你们抽出时间。
在 Twitter 上关注我们 @no prior pod。如果你想看我们的脸，请订阅我们的 YouTube 频道。在 Apple Podcasts、Spotify 或任何你收听播客的地方关注本节目，这样你每周都能收到新一集。在 no-priors.com 注册电子邮件或查找每集节目的文字记录。
[音乐]