小乐数学科普：陶哲轩长文阐述机器辅助证明——译自美国数学会通讯AMS Notice 202501

图源：Terence Tao|AMS Notice

几个世纪以来，数学家一直依靠计算机（人类、机械或电子）和机器来协助他们的研究（如果考虑到算盘等早期计算工具，甚至几千年）。例如，自从纳皮尔（John Napier，1550 - 1617）等人的早期对数表以来，数学家就知道构建数学对象的大型数据集来执行计算和做出猜想的价值。勒让德（Adrien-Marie Legendre，1752 - 1833）和高斯（Carl Friedrich Gauss，1777 - 1855）使用人类计算机编制的大素数表来猜想现在所谓的素数定理（PNT）；一个半世纪后，伯奇（Bryan John Birch，1931 -）和斯温纳顿-戴尔（Peter Swinnerton-Dyer，1927 - 2018）同样使用早期电子计算机生成有限域上椭圆曲线的足够数据，以提出他们自己对这些对象的著名猜想（即BSD猜想）。毫无疑问，许多读者已经利用了最广泛的数学数据集之一——整数数列在线百科全书（OEIS），它产生了无数猜想以及在不同数学领域之间意想不到的联系，并为研究人员提供了一个有价值的数学对象的文献搜索引擎。他们不知道该数学对象的名称，但可以将其与整数序列相关联。在21世纪，此类大型数据库还可以作为机器学习算法的关键训练数据，这些算法有望实现自动化或者至少大大简化数学猜想和联系的生成过程。

除了数据生成之外，计算机的另一个重要用途是科学计算，如今科学计算被大量用于数值求解微分方程和动力系统，或计算大型矩阵或线性算子的统计数据。这种计算的早期例子出现在1920年代，当时亨德里克·洛伦兹（Hendrik Lorentz，1853 - 1928）组建了一组人类计算机来模拟阿夫鲁戴克大坝（Afsluitdijk，当时荷兰正在建设的一座水坝）周围的流体流动；除其他外，该计算因开创了现在标准的浮点运算装置而闻名。但现代计算机代数系统（CAS，例如Magma、SAGEMath、Mathematica、Maple等）以及更通用的编程语言可以远远超出传统的“数字运算”；它们现在通常用于执行代数、分析、几何、数论和许多其他数学分支中的符号计算。由于舍入误差和不稳定性，某些形式的科学计算是众所周知的不可靠，但人们通常可以用更严格的方法来代替这些方法（例如，用区间算术代替浮点算术），这可能会增加运行时间或内存使用量。

计算机代数系统的近亲是可满足性（SAT，satisfiability）求解器和可满足性模理论 (SMT，satisfiability modulo theory) 求解器，它们可以根据某些受限制的假设集合对结论进行复杂的逻辑推导，并为每个此类推导生成证明证书。当然，可满足性是一个 NP完全问题，因此这些求解器的规模不会超过某个临界点。以下是使用SAT求解器证明结果的典型示例：

定理 0.1 （布尔勾股数三元组定理【HKM16】）

集合{1, ⋯ ,7824}的元素可以分为两类，使得每一类中都不包含勾股数三元组——满足a²+b²=c²的(a,b,c)；然而，对于集合{1, ⋯ ,7825}这是不可能的。

该证明需要4个CPU年的计算并生成200TB的命题证明，后来被压缩到68GB。

当然，数学家也经常使用计算机来完成日常任务，例如撰写论文以及与合作者交流。但近几十年来，出现了几种利用计算机辅助数学研究的有前途的新方法：

• 机器学习算法可用于发现新的数学关系，或生成数学问题的潜在示例或反例。

  
  

• 形式证明助手可用于验证证明（以及大语言模型的输出），允许真正大规模的数学协作，并帮助构建数据集来训练上述机器学习算法。

  
  

• ChatGPT等大语言模型（有可能）被用来使其他工具更容易、更快速地使用；它们还可以建议证明策略或相关工作，甚至直接生成（简单的）证明。

这些类型的工具中的每一种都已经在不同的数学领域找到了合适的应用，但我发现特别有趣的是将这些工具组合在一起的可能性，用一种工具抵消另一种工具的弱点。例如，形式证明助手和计算机代数包可以过滤掉现在臭名昭著的大语言模型看似合理的废话的“幻觉”倾向，而反之，这些模型可以帮助自动化证明形式化中更繁琐的方面，并提供用于运行复杂符号或机器学习算法的自然语言界面。其中许多组合仍仅处于概念验证开发阶段，该技术需要一定的时间才能变得成熟起来成为数学家真正有用且可靠的工具。然而，早期的实验似乎确实令人鼓舞，我们应该期待在不久的将来会出现一些令人惊讶的新数学研究模式的演示；它不是科幻小说中可以自主解决复杂数学问题的超级智能人工智能，而是一个有价值的助手，可以提出新想法、过滤错误、执行例行案例检查、数值实验和文献评审任务，让人类数学家能够在项目中注重对高层概念的探索。

当然，计算是使用计算机执行的这一事实并不能自动保证其正确。计算可能会产生数值误差，例如由于用离散近似值替换连续变量或方程而引起的误差。代码中可能会无意中引入错误，或者输入数据本身可能包含不准确之处。即使计算机用来运行代码的编译器也可能存在缺陷。最后，即使代码完美执行，代码正确计算的表达式也可能不是数学论证真正想要的表达式。

早期的计算机辅助证明遇到了许多这样的问题。例如，凯尼斯·阿佩尔（Kenneth Appel，1932 - 2013）和沃夫冈·哈肯（Wolfgang Haken，1928 - 2022）在1976年对四色定理【AH89】的原始证明围绕着一系列1834个需要遵守两个性质称为“可归约性”（reducibility）和“不可避免性”（unavoidability）的图。可以通过每次将每个图输入一个定制的软件来检查可归约性；但不可避免的是，需要进行繁琐的计算，包括数百页的缩微胶片——通过哈肯的女儿Dorothea Blostein（多萝西娅·布洛斯坦）的英勇努力手工验证——最终包含多个（可修复的）错误。1994年，Robertson、Sanders、Seymour和 Thomas【RSST96】试图使Appel–Haken证明的计算部分完全可由计算机验证，但最终却产生了一个更简单的论证（仅涉及633个图，以及验证不可避免性的更简单的程序），可以通过用任意数量的标准编程语言编写的计算机代码更有效地验证。

证明助手将这种形式化更进一步，作为一种特殊类型的计算机语言，其设计目的不是执行纯粹的计算任务，而是验证逻辑或数学论证结论的正确性。粗略地说，数学证明中的每个步骤都对应于该语言中的多行代码，并且只有在证明有效的情况下才能编译整个代码。现代证明助手，例如Coq、Isabelle或Lean，有意尝试模仿数学写作的语言和结构，尽管它们在许多方面通常更加挑剔。举一个简单的例子，为了解释一个数学表达式，例如aᵇ,形式的证明助手可能需要精确指定基础变量a,b的“类型”（例如，自然数、实数、复数），以便确定正在使用哪种求幂运算（这对于诸如0⁰的表达式尤其重要，在不同的求幂概念下，其解释略有不同）。人们投入了大量精力来开发自动化工具和广泛的数学结果库来管理形式证明的这些低级方面，但在实践中，数学论证的“明显”部分通常比“重要”部分需要更长的时间才能形式化。举一个例子：给定三个集合A₁,A₂,A₃，数学家可能会相互切换使用笛卡尔积(A₁×A₂)×A₃, A₁×(A₂×A₃)和∏_{i∈{1,2,3}}Aᵢ，因为它们“显然”是“同一”对象；但在大多数数学形式化中，这些乘积实际上并不相同，并且论证的形式化版本可能需要投入一部分证明来在这些空间之间建立适当的等价性，并确保涉及该乘积的一个版本的陈述对于另一个版本继续成立。

由于这个和其它的原因，将人类数学家（即使是非常仔细的数学家）编写的证明转换为在形式证明助手中编译的形式证明的任务相当耗时，尽管随着时间的推移，这个过程逐渐变得更加高效。上述四色定理由Werner和Gonthier于2005年【Gon08】在Coq中形式化。关于𝐑³中对单位球最密堆积的臭名昭著的开普勒猜想的证明由Hales和Ferguson在1998年【Hal05】的一个非常复杂的（计算机辅助的）证明中证明。2003年，Hales启动了Flyspeck项目来形式化地验证证明，预计需要20年才能完成，尽管最终通过Hales和其他21位贡献者的合作，“仅”用了11年就实现了这一目标【HAB⁺17】。最近，舒尔茨（Peter Scholze，1987 -）于2019年启动了“液体张量实验” 【Com22】，形式验证了他和克劳森（Dustin Clausen）关于凝聚态数学理论中“液体向量空间”的某个Ext群消失的基本定理。人类写的证明“只有”十页长，尽管包含大量凝聚态数学的先决材料；尽管如此，通过大量的协作努力，Lean的形式化花费了大约18个月的时间。我本人领导了一项关于高尔斯、格林、曼纳斯和我自己的加性组合猜想【GGMT23】最近证明的形式化工作【Tao23】；人工编写的证明长达33页，但基本上是自给自足的，大约20名合作者组成的小组在三周内将其形式化。有些数学领域比其他领域更难以形式化；凯文·巴扎德（Kevin Buzzard，1968 -）最近宣布了一项形式化费马大定理证明的项目，他估计至少需要五年时间完成。

考虑到所需的所有努力，数学证明的形式化工作对数学的价值是什么？最明显的是，它为给定结果的正确性提供了极高的置信度，这对于有争议或因强烈吸引虚假证明而臭名昭著的结果特别有价值，或者对于审阅人愿意逐行验证此类特别冗长的证明的领域尤其供不应求。（理论上，证明助手编译器中仍然可能存在隐藏的缺陷 - 故意将其保持得尽可能小以减少这种可能性 - 或者结果的形式声明中使用的定义可能在微妙但重要的方面与人类可读的陈述有所不同，但这种情况不太可能发生，特别是如果形式证明密切跟踪人类编写的证明的前提下。）形式化过程通常会发现人类证明中的小问题，有时可以揭示论证的简化或强化，例如通过揭示一个看似重要的假设在引理中实际上是不必要的，或者可以使用低功效但更通用的工具来代替高级但专门的工具。采用现代语言（例如Lean）的形式化项目通常会将项目过程中生成的许多基本数学结果贡献到公共数学库中，这使得未来形式化项目更容易进行。

但形式证明助手也可以实现数学教育和协作的新模式。几个实验项目正在进行中，以获取形式证明并将其转换为更易于人类理解的形式，例如一段交互式文本，其中论证中的各个步骤可以扩展为更详细的内容或折叠为高级摘要；这可能是一种特别适合未来数学教科书的格式。传统的数学合作很少涉及超过五个左右的共同作者，部分原因是每个共同作者都需要信任和验证其他人的工作；但形式化项目通常会涉及数十名之前没有互动过的人，这正是因为形式证明助手允许项目中的各个子任务独立于其他子任务进行精确定义和验证。可以想象，这些证明助手还可以允许类似的分工来生成新的数学结果，从而允许比以前的在线协作（例如“Polymath”项目【Gow10】，其规模由于需要对讨论进行人工审核而受到限制）规模大得多的高度并行和众包协作。随着时间的推移，其他科学或软件工程项目中已经建立的大型合作也可能在研究数学中变得司空见惯。一些贡献者可能扮演“项目经理”的角色，例如专注于建立精确的“蓝图”，将项目分解为更小的部分，而其他贡献者则可以专门研究项目的各个组成部分，而不必具备理解整个项目所需的所有专业知识。

然而，在此之前，形式化过程需要变得更加高效。“de Bruijn因子”（编写正确的形式证明与正确的非形式证明的难度之间的比率）仍然远高于1（我估计约为20)，但在下降中。我相信将该比率降至1以下不存在根本障碍，尤其是因为AI、SMT求解器和其他工具的集成度不断提高；这将给我们的领域带来变革。

机器学习是指训练计算机执行复杂任务的一系列技术，例如预测与来自非常广泛的类别的给定输入相对应的输出，或者辨别数据集中的相关性和其他关系。许多流行的机器学习模型使用某种形式的神经网络来编码计算机如何执行任务。这些网络是由大量简单运算（线性和非线性）组合在一起形成的许多变量的函数；通常，人们会为这样的网络分配某种奖励函数（或损失函数），例如通过根据训练数据集凭经验测量其性能，然后执行计算密集型优化以找到该网络的参数选择使得奖励函数尽可能大（或损失函数尽可能小）。这些模型具有无数的实际应用，例如图像和语音识别、推荐系统或欺诈检测。然而，它们通常不能提供强有力的准确性保证，特别是当应用于与训练数据集显著不同的输入时，或者当训练数据集有噪声或不完整时。此外，模型通常是不透明的，因为很难从模型中提取人类可以理解的解释来说明模型为什么做出特定的预测，或者理解模型的一般行为。因此，这些工具乍一看似乎不适合研究数学，因为人们既希望得到严格的证明，又希望对论证有直观的理解。

尽管如此，最近出现了一些有前景的用例，即适当选择的机器学习工具可以产生或至少提出新的严格数学，特别是与其他可以验证这些工具输出的更可靠技术相结合时。例如，流体方程数学理论（例如欧拉方程或纳维-斯托克斯N-S方程）的一个基本问题是能够严格证明解u在有限时间内从光滑的初始数据开始有限时间内爆破。最臭名昭著的例子涉及三维不可压缩纳维-斯托克斯方程，该方程的解是（未解决的）千禧年奖问题之一；这仍然遥不可及，但最近在其他流体方程方面取得了进展，例如二维的Boussinesq方程（三维不可压缩欧拉方程的简化模型）。建立这种奇点（singularity）的一种途径是构建自相似的爆破解u，由解出一个更简单的偏微分方程（PDE）的低维函数U描述。该偏微分方程的封闭形式解似乎不可用；但如果能够产生这个偏微分方程的足够高质量的近似解Ũ（近似服从某些边界条件），可以通过应用微扰理论严格证明精确解U（例如基于不动点定理的理论）。传统上，人们会使用数值PDE方法来尝试产生这些近似解Ũ，例如，通过将偏微分方程离散化为差分方程（difference equation），但使用此类方法获得具有所需精度水平的解的计算成本可能很高。Wang、Lai、Gómez-Serrano和Buckmaster【WLGSB23】于2019年提出了另一种方法，他们使用经过训练的物理信息神经网络（PINN，Physics Informed Neural Network）来生成函数Ũ，可以最小化一个合适的损失函数，该函数度量了近似遵守所需偏微分方程和边界条件的程度。由于这些函数Ũ通过神经网络而不是方程的离散版本生成，它们可以更快地生成，并且可能不易受到数值不稳定的影响。事实证明，Chen和Hou的同期工作【CH22】能够使用更传统的数值方法为该方程建立有限时间爆破解；然而，机器学习范式显示出作为此类偏微分方程问题的补充方法的巨大潜力。例如，我们可以设想一种混合方法，其中人类数学家首先提出一个爆破模拟，然后神经网络尝试找到一个粗略的近似解，然后使用更传统的数值方法将该解细化得足够准确，使得可以对其应用严格的稳定性分析。

机器学习在数学中应用的另一个例子是纽结理论（knot theory）领域。结具有极其多样化的拓扑不变量：结的符号差（signature）是与以结为边界的表面（Siefert曲面）的同调性相关的整数；结的Jones琼斯多项式可以使用辫子（braid）的表示理论来描述；大多数结（不包括环面结torus knot）其补（complement）具有典范双曲几何，可用于描述许多双曲不变量，例如双曲体积等等。先验地，这些来自不同数学领域的不变量之间的相互关系并不明显。然而，2021年，Davies、Juhász、Lackenby和Tomasev【DJLT21】通过机器学习研究了这个问题。通过在现有的近200万个结（加上100万个随机生成的额外的结）的数据库上训练神经网络，他们能够使该神经网络模型从大约两打双曲不变量中高精度地预测结的符号差。然而，生成的预测函数非常不透明，并且最初并没有揭示出关于符号差和双曲不变量之间的精确关系的更多见解。然而，可以通过一种称为显著性分析（saliency analysis）的简单工具进一步进行，粗略地说，该工具测量每个单独的双曲不变量对预测函数的影响。该分析表明，在使用的两打双曲不变量中，只有其中三个（纵向平移以及子午平移的实部和复数部分）对预测函数有显著影响。通过视觉上检查这三个不变量的符号差散点图，作者能够推测出这些数量之间更容易理解的关系。进一步的数值反驳了他们最初的猜想，但提出了他们能够严格证明的猜想的修改版本。机器生成的猜想与人类使用理论进行验证（和修改）之间的相互作用是一个有前途的范式，似乎适用于许多其他数学领域。

机器学习的许多应用需要大量的训练数据，理想情况下以某种标准化格式（例如数字向量）表示，以便现有的机器学习算法可以相对轻松地应用于其中。数据的精确表示至关重要；机器学习算法可以很容易地在一种数据表示中发现数据不同组成部分之间的相关性，但在另一种数据表示中几乎不可能找到。虽然数学的一些领域开始编制有用对象的大型数据库（例如，结、图或椭圆曲线），但仍然有许多重要类别的更模糊定义的数学概念尚未系统地放入可用于机器学习的形式中。例如，回到偏微分方程的例子，文献中研究了数千种不同的偏微分方程，但通常在符号和项的代数排列方面具有很大的可变性，而且没有什么类似于通常所研究的偏微分方程的标准数据库（例如，研究它们是椭圆形、抛物线形还是双曲形；解的存在性和唯一性、守恒定律等已知的信息）。这样的数据库可能有助于根据其他偏微分方程的结果对一个偏微分方程的行为进行推测性预测，或者建议从一种偏微分方程到另一种偏微分方程的可能类比或化简；但由于缺乏任何规范范式来表示此类方程（或至少缺乏识别它们的“指纹” 【BT13】），因此目前构建这样的数据库都非常困难，更不用说将其输入神经网络了。可以想象，未来的证明形式化和人工智能的进步可能会使生成和利用此类数据库（可能包含“真实世界”和“合成”数据集）变得更加可行。

大语言模型（LLM）是一种相对较新的机器学习模型，适合对极其广泛和大型的自然语言文本数据集进行训练。一种流行的大语言模型是GPT（Generative Pre-trained Transformer生成式预训练转换器），顾名思义，它是围绕Transformer模型（一种神经网络变体，旨在预测字符串中的下一个单词即“token词元”，并保留对字符串早期单词的一些长期“注意力”，以模拟句子的上下文）构建的。通过迭代该模型，人们可以对给定的文本提示（prompt）生成冗长的文本响应。当使用少量数据进行训练时，此类模型的输出并不令人印象深刻，例如，并不比尝试在智能手机上迭代“自动完成”文本输入功能复杂多少，但经过对极大且多样化的数据集进行大量训练后，这些模型的输出可以令人惊讶地连贯，甚至具有创造性，并且可以生成乍一看很难与人类书写区分开的文本，尽管仔细检查后，输出通常是无意义的，并且与任何基本事实没有联系，这种现象被认为是“幻觉”（hallucination）。

人们当然可以尝试应用这种通用的LLM来尝试直接解决数学问题。有时，结果可能相当令人印象深刻；例如布贝克（Bubeck）等人记录了一个案例，其中强大的大语言模型GPT-4能够提供2022年国际数学奥林匹克问题的完整且正确的证明，该问题并不在该模型的训练数据集中。相反，该模型不太适合执行精确计算，甚至基本算术；在一个例子【BCE⁺23】中，当要求计算表达式7×4 + 8×8时，GPT-4立即给出了错误答案120，然后继续通过分步过程来证明计算的合理性返回正确答案92。当被问及这一差异时，GPT-4只表示其最初的猜测是一个“拼写错误”（typo）。这些问题可以通过使用GPT-4的“插件”得到一定程度的补偿，其中GPT-4被训练为向外部工具（例如Wolfram Alpha）发送特定类型的查询（例如数学计算），而不是通过其内部模型猜测答案，尽管目前工具之间的集成还不是无缝的。类似地，最近的概念验证【RPBN⁺23】已经表明，LLM可用于查找组合学和计算机科学中各种问题的示例，这些示例优于以前的人类生成的示例，方法是要求这些模型生成程序来创建此类示例，而不是尝试直接构建示例，然后使用另一种语言执行该程序来可靠地验证输出的质量，然后将其发送回原始模型以提示其对猜测进行改进。最近在使用LLM来增强现有符号证明引擎以解决狭窄类别的数学问题（例如奥林匹克几何问题【TWL⁺24】）方面也取得了进展.

在我自己的GPT-4实验中（可以在 https://terrytao.wordpress.com/mastodon-posts/ 找到），我发现最高效的用例是生成各种语言的基本计算机代码（Python、SAGE、LaTeX、Lean、正则表达式等），或者清理凌乱且无组织的数据集（例如，在起初提供GPT-4一些所需参考书目条目格式的示例后，让它将互联网上抓取的一堆参考文献整理成连贯的LaTeX参考书目）。在这种情况下，它通常会在第一次尝试时产生令人满意或接近令人满意的输出，只需进行少量修改即可获得我正在寻求的输出类型。我在让GPT-4为实际数学问题推荐相关文献或技术方面也取得了一些有限的成功。在一个测试用例中，我问它如何计算独立随机变量之和的尾部概率的指数衰减率，以在不给它提供大偏差理论（large deviation theory）等关键词前提下，评估它是否知道这方面的相关定理（Cramér定理）。事实证明，GPT-4并没有准确定位这个定理，而是产生了一串数学废话，但奇怪的是，它确实引用了对数矩生成函数（logarithmic moment generating function），这是Cramér定理陈述中的一个关键概念，即使它似乎并不确切地“知道”这个函数与问题的相关性。在另一个实验中，我向GPT-4询问如何证明我正在研究的组合恒等式的建议。它给出了一些我已经考虑过的建议（渐近分析、归纳、数值）以及一些通用建议（简化表达式、寻找类似问题、理解问题），而且还提出了一种技术（生成函数）我只是忽略了这一点，最终很容易地解决了这个问题。另一方面，这样的建议列表对于新手数学家来说可能没什么用，因为他们没有足够的经验来独立评估每个建议的有用性。尽管如此，我看到这些工具在提取用户对一个问题的潜在知识方面的作用，只需成为一个好的倾听者并提出足够用户给出专业评估的合理相关的想法即可。

Github Copilot（副驾驶）是另一个GPT模型，已集成到多个流行的代码编辑器中。它经过不同语言的大型代码数据集的训练，旨在利用上下文线索（例如代码中其他地方要执行的任务的非形式描述）为部分编写的代码提供自动完成建议。我发现它对于编写数学LaTeX以及在Lean中形式化非常有效；事实上，它在我写作时建议了几句话，从而帮助我写了这篇文章，其中许多句子我在最终版本中保留着或进行了轻微编辑。虽然其建议的质量差异很大，但有时它可以表现出对文本意图的模拟理解的不可思议的水平。例如，在编写另一篇关于如何估计积分的阐述性LaTeX笔记时，我描述了如何将积分分解为三个部分，然后详细说明了如何估计第一部分。然后Copilot立即建议如何通过类似的方法来估计第二部分，并以完全正确的方式改变变量。这些频繁经历使我在LaTeX和Lean的写作中获得了小幅但明显的加速，我预计这些工具在未来会变得更加有用，因为可以根据个人写作风格和喜好“微调”这些模型。

上面讨论的各种技术都有非常不同的优点和缺点，而且就其目前的发展水平而言，没有一种技术适合作为数学家的通用工具，能与LaTeX或arXiv等无处不在的平台相媲美。然而，最近有一些有希望的实验可以通过将两种或多种单独的技术结合在一起来创建更令人满意的工具。例如，在生成证明时对抗LLM的幻觉性质的一种可行方法是要求模型以形式证明助手的语言格式化其输出，并将助手生成的任何错误作为反馈发送回模型。这个组合系统似乎适合生成简单命题的简短证明【YSG⁺23】；由于此类任务通常是有效形式化证明的限制因素，因此这种范式可以大大加快这种形式化的速度，特别是如果这些模型在形式化证明（而不是一般文本）上进行微调，并与更传统的自动化定理证明方法集成，例如SMT求解器的部署。

由于能够接受自然语言输入，LLM还可能是一个用户友好的界面，允许没有特定软件专业知识的数学家使用高级工具。如前所述，我和许多其他人已经经常使用此类模型来生成各种语言的简单代码（包括符号代数包），或创建复杂的图表和图像；似乎可以合理地预期，在不久的将来，人们还可以通过此类模型进行通信，仅使用高级会话指令来设计和操作像机器学习模型这样复杂的东西。更雄心勃勃的是，人们可能希望最终能够通过用自然语言向人工智能解释结果来生成完整的研究论文（初稿），并完成形式验证，人工智能将尝试形式化结果的每一步并在需要澄清时询问作者。

当前形式的形式化证明验证的人力密集性质意味着当前研究论文的很大一部分实时完全形式化是不可行的。然而，许多已经用于验证研究论文中特定计算密集型部分的工具（例如数值积分或 PDE求解器、符号代数计算或使用SMT求解器建立的结果）似乎可以进行修改之后出具形式证明证书。此外，可以以这种方式形式化的计算类别可以从当前实践中大大扩展。仅举一个例子，在偏微分方程领域，通常会使用大量计算来估计涉及一个或多个未知函数（例如一个偏微分方程的解）的某些积分表达式，并使用各种函数空间范数中此类函数的界限（例如Sobolev索博列夫空间范数），以及标准不等式（例如，Hölder霍尔德不等式和Sobolev索博列夫不等式），以及各种恒等式，例如分部积分或积分符号下的微分。此类计算虽然是常规计算，但可能包含不同严重程度的拼写错误（例如符号错误），并且仔细审阅可能会很乏味，因为计算本身除了验证最终估计值是否成立之外几乎没有提供任何见解。可以想象，可以开发工具来以自动或半自动的方式建立此类估计，并且当前此类估计的冗长且无启发性的证明可以由形式证明证书的链接取代。更雄心勃勃的是，人们可能能够要求未来的AI人工智能工具在给定一组初始假设和方法的情况下产生最佳估计，而无需首先进行一些纸笔计算来猜测估计值是什么。目前，可能估计的状态空间太复杂，无法以这种方式自动探索；但我认为随着技术的进步，这种自动化没有理由无法实现。当这种情况成为现实时，目前尚不可行的大规模的数学探索就成为可能。继续以偏微分方程为例，该领域的论文通常一次研究一两个方程；但在未来，人们可能能够同时研究数百个方程，也许只为一个方程给出完整的论证，然后让人工智能工具将论证适应一大族的相关方程，在推广的论点非常规时询问作者是否有必要扩展。这种大规模数学探索的一些提示开始在数学的其他领域出现，例如图论中猜想的自动探索【Wag21】。

目前尚不清楚这些实验中哪一个最终将最成功地为典型的数学家带来先进的计算机辅助。一些概念证明目前无法扩展，特别是那些依赖于计算极其密集（且通常是专有）的人工智能模型，或需要大量专家人工输入和监督的证明。然而，我对探索可能性空间的各种努力感到鼓舞，并相信在不久的将来会有更多执行机器辅助数学的新方法的例子。

机器辅助证明的主题相当广泛，分布在数学、计算机科学甚至工程学的各个领域；虽然每个单独的子领域都有大量的活动，但直到最近才努力建立一个更加统一的社区，将此处列出的所有主题汇集在一起。因此，目前很少有地方可以找到对这些快速发展的数学模式的全面调查。一个起点是2023年6月美国国家科学院“人工智能辅助数学推理”研讨会的会议记录【Kor23】（作者是该研讨会的联合组织者之一）；作为该研讨会的成果之一，Talia Ringer领导了一项为数学资源编译AI的工作，其结果可以在https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0 中找到。

例如，该文档中有一个指向“自然数字游戏”的链接，这是一种开始熟悉Lean证明辅助语言的易于访问和交互的方式。这里讨论的许多例子也取自2023年2月的IPAM研讨会“机器辅助证明”（作者也参与共同组织），该研讨会的演讲可以在网上找到。

感谢匿名审稿人的指正和建议。

[AH89]

Kenneth Appel and Wolfgang Haken, Every planar map is four colorable, Contemporary Mathematics, vol. 98, American Mathematical Society, Providence, RI, 1989. With the collaboration of J. Koch, DOI 10.1090/conm/098. MR1025335

[BT13]

Sara C. Billey and Bridget E. Tenner, Fingerprint databases for theorems, Notices Amer. Math. Soc. 60 (2013), no. 8, 1034–1039, DOI 10.1090/noti1029. MR3113227

[BCE⁺23]

Sébastien Bubeck, Varun Chandrasekaran, Ronen Eldan, Johannes Gehrke, Eric Horvitz, Ece Kamar, Peter Lee, Yin Tat Lee, Yuanzhi Li, Scott Lundberg, Harsha Nori, Hamid Palangi, Marco Tulio Ribeiro, and Yi Zhang, Sparks of artificial general intelligence: Early experiments with GPT-4, Preprint, arXiv:2303.12712, 2023.

[CH22]

Jiajie Chen and Thomas Y. Hou, Stable nearly self-similar blowup of the 2D Boussinesq and 3D Euler equations with smooth data, parts I and II, 2022. arXiv:2210.07191; arXiv:2305.05660.

[Com22]

Johan Commelin, Liquid tensor experiment (German, with German summary), Mitt. Dtsch. Math.-Ver. 30 (2022), no. 3, 166–170, DOI 10.1515/dmvm-2022-0058. MR4469845

[DJLT21]

Alex Davies, András Juhász, Marc Lackenby, and Nenad Tomasev, The signature and cusp geometry of hyperbolic knots, Preprint, arXiv:2111.15323, 2021.

[Gon08]

Georges Gonthier, Formal proof—the four-color theorem, Notices Amer. Math. Soc. 55 (2008), no. 11, 1382–1393. MR2463991

[Gow10]

W. T. Gowers, Polymath and the density Hales-Jewett theorem, An irregular mind, Bolyai Soc. Math. Stud., vol. 21, János Bolyai Math. Soc., Budapest, 2010, pp. 659–687, DOI 10.1007/978-3-642-14444-8_21. MR2815619

[GGMT23]

W. T. Gowers, Ben Green, Freddie Manners, and Terence Tao, On a conjecture of Marton, Preprint, arXiv:2311.05762, 2023.

[HAB⁺17]

Thomas Hales, Mark Adams, Gertrud Bauer, Tat Dat Dang, John Harrison, Le Truong Hoang, Cezary Kaliszyk, Victor Magron, Sean McLaughlin, Tat Thang Nguyen, Quang Truong Nguyen, Tobias Nipkow, Steven Obua, Joseph Pleso, Jason Rute, Alexey Solovyev, Thi Hoai An Ta, Nam Trung Tran, Thi Diep Trieu, Josef Urban, Ky Vu, and Roland Zumkeller, A formal proof of the Kepler conjecture, Forum Math. Pi 5 (2017), e2, 29, DOI 10.1017/fmp.2017.1. MR3659768

[Hal05]

Thomas C. Hales, A proof of the Kepler conjecture, Ann. of Math. (2) 162 (2005), no. 3, 1065–1185, DOI 10.4007/annals.2005.162.1065. MR2179728

[HKM16]

Marijn J. H. Heule, Oliver Kullmann, and Victor W. Marek, Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer, Theory and applications of satisfiability testing—SAT 2016, 2016, pp. 228–245, DOI 10.1007/978-3-319-40970-2_15. MR3534782

[Kor23]

Samantha Koretsky (ed.), Artificial intelligence to assist mathematical reasoning: Proceedings of a workshop, National Academies Press, 2023, DOI 10.17226/27241.

[RSST96]

Neil Robertson, Daniel P. Sanders, Paul Seymour, and Robin Thomas, A new proof of the four-colour theorem, Electron. Res. Announc. Amer. Math. Soc. 2 (1996), no. 1, 17–25, DOI 10.1090/S1079-6762-96-00003-0. MR1405965

[RPBN⁺23]

Bernardino Romera-Paredes, Mohammadamin Barekatain, Alexander Novikov, Matej Balog, M. Pawan Kumar, Emilien Dupont, Francisco J. R. Ruiz, Jordan S. Ellenberg, Pengming Wang, Omar Fawzi, Pushmeet Kohli, and Alhussein Fawzi, Mathematical discoveries from program search with large language models, Nature 625 (December 2023), no. 7995, 468–475, DOI 10.1038/s41586-023-06924-6.

[Tao23]

Terence Tao, Formalizing the proof of PFR in Lean4 using Blueprint: a short tour, 2023. https://terrytao.wordpress.com/2023/11/18

[TWL⁺24]

Trieu H. Trinh, Yuhuai Wu, Quoc V. Le, He He, and Thang Luong, Solving olympiad geometry without human demonstrations, Nature 625 (January 2024), no. 7995, 476–482, DOI 10.1038/s41586-023-06747-5.

[Wag21]

Adam Zsolt Wagner, Constructions in combinatorics via neural networks, Preprint, arXiv:2104.14516, 2021.

[WLGSB23]

Y. Wang, C.-Y. Lai, J. Gómez-Serrano, and T. Buckmaster, Asymptotic self-similar blow-up profile for three-dimensional axisymmetric Euler equations using neural networks, Phys. Rev. Lett. 130 (2023), no. 24, Paper No. 244002, 6, DOI 10.1103/physrevlett.130.244002. MR4608987

[YSG⁺23]

Kaiyu Yang, Aidan M. Swope, Alex Gu, Rahul Chalamala, Peiyang Song, Shixing Yu, Saad Godil, Ryan Prenger, and Anima Anandkumar, LeanDojo: Theorem proving with retrieval-augmented language models, Preprint, arXiv:2306.15626, 2023.

https://www.ams.org/journals/notices/202501/noti3041/noti3041.html

https://terrytao.wordpress.com/mastodon-posts/

https://docs.google.com/document/d/1kD7H4E28656ua8jOGZ934nbH2HcBLyxcRgFDduH5iQ0