引言：AI在数学领域的新突破
计算机长期以来在数值计算方面表现出色，但它们并未对人类数学家构成实质性威胁。直到最近，它们在高中级别的数学竞赛中仍难以与人类匹敌。然而，谷歌DeepMind团队开发的AlphaProof系统彻底改变了这一局面，该系统在2024年国际数学奥林匹克竞赛(IMO)中达到了银牌选手的水平，在全球最负盛名的大学生数学竞赛中仅以一分之差无缘金牌。这一成就标志着人工智能在数学证明领域的重要突破。
真正的理解：AI如何掌握数学本质
计算机在数学竞赛中表现不佳的原因在于，尽管它们在计算能力上远超人类，但在高级数学所需的逻辑和推理方面却相对薄弱。换句话说，计算机擅长快速执行计算，但在理解为何进行这些计算方面存在局限。虽然加法等操作看似简单，但人类能够基于加法的定义进行半形式化证明，或采用完全形式的皮亚诺算术(Peano arithmetic)，通过公理定义自然数和加法等操作的性质。
要执行证明，人类必须理解数学的基本结构。数学家构建证明的方式、达到结论所需的步骤数量以及这些步骤设计的巧妙程度，都体现了他们的智慧、独创性和数学优雅性。正如DeepMind研究员兼AlphaProof研究的主要作者Thomas Hubert所言："你知道，伯特兰·罗素曾出版了一本500页的书来证明一加一等于二。"
DeepMind团队希望开发一种能在这一层面理解数学的AI。这项工作始于解决AI的常见问题：训练数据的缺乏。
数学问题翻译器：从自然语言到形式化系统
像ChatGPT这样由大型语言模型驱动的AI系统从数十亿页文本中学习。由于训练数据库中包含数学相关的文本——所有手册和著名数学家的著作——它们在证明数学命题方面取得了一定成功。但它们的操作方式存在局限性：它们依赖使用巨大的神经网络来预测响应提示时生成的序列中的下一个词或标记。其推理本质上是统计性的，这意味着它们只是返回听起来"正确"的答案。
DeepMind不需要AI听起来正确——这在高级数学中远远不够。他们需要AI"真正正确"，保证绝对确定性。这要求一个全新的、更加形式化的训练环境。为此，团队使用了一个名为Lean的软件包。
Lean是一个帮助数学家编写精确定义和证明的计算机程序。它依赖于一种精确的编程语言，也称为Lean，数学命题可以翻译成这种语言。一旦翻译或形式化的语句被上传到程序中，它就可以检查是否正确，并返回"这是正确的"、"缺少某些内容"或"你使用了尚未证明的事实"等反馈。
问题是，大多数可以在网上找到的数学命题和证明都是用自然语言编写的，如"设X为自然数集..."——用Lean编写的语句数量相当有限。Hubert表示："使用形式语言的主要困难在于数据非常少。"为了解决这个问题，研究人员训练了一个Gemini大型语言模型，将数学命题从自然语言翻译成Lean。该模型像一个自动形式化工具，产生了约8000万条形式化的数学命题。
虽然这不完美，但团队设法利用了这一点。Hubert声称："有很多方法可以利用近似翻译。"
学习思考：AlphaProof的架构设计
DeepMind为AlphaProof提出的想法是使用他们在国际象棋、围棋和将棋-playing AlphaZero AI系统中使用的架构。在Lean和一般数学中构建证明应该只是需要掌握的另一种"游戏
