（视觉中国/图）
随着GPT热潮的不断发展，包括ChatGPT在内的大型语言模型（Large Language Model；LLM）开始逐渐进入各种原来被认为是人类智力活动专属的领域当中。例如，菲尔兹奖得主、华裔数学家陶哲轩就在一篇博客中宣称，他已经开始使用GPT-4来协助自己的工作。而2023年7月27日发布在预印本网站（arXiv）上的一篇由加州理工、英伟达、MIT等机构的学者共同撰写的论文声称，他们构建了一个基于开源LLM的定理证明器。似乎一夜之间，AI就攻陷了数学，这个人类智慧最纯粹的领域之一。
实际上，追本溯源起来，数学家寻找自动化证明的过程，已经有一百多年的历史了。甚至计算机的诞生与发展，也与这一探寻过程有着密不可分的关系。
数学基础与哥德尔不完备定理
在1900年4月27日英国皇家学会的一次演讲上，物理学家开尔文男爵发表了著名的物理学“两朵乌云”的演讲。后来的事情大家都知道了，两朵乌云掀起了狂风暴雨，从中诞生了二十世纪现代物理学的两大支柱相对论和量子力学。
就在开尔文男爵发表演讲的同一年，数学家大卫希尔伯特在巴黎举行的第二届国际数学家大会上，作了题为《数学问题》的演讲，提出了二十三道他认为最重要的数学问题。这些问题随后被称作“希尔伯特问题”或者“希尔伯特的23个问题”。针对这些问题的研究，在很大程度上促进了二十世纪数学的发展。
在希尔伯特提出的这23个问题当中，就有诸如“连续统假设”“算术公理之相容性”“公理化物理”这样涉及数学以及科学基础的问题。这些问题的提出，来源于希尔伯特的雄心壮志：他希望能够建立起一套统一的数学公理化体系。不止于此，在公理化体系之上，他还有一个更加宏大的设想，那就是所谓的“希尔伯特形式主义纲领”。
按照希尔伯特的设想，他想要建立的形式化的数学公理体系应该满足三个条件。即：完备性：可以发现所有数学真命题；自洽性：数学内部不存在矛盾；可决定性：能够判断每一个数学命题的真伪。
作为数学家的希尔伯特，他所关心的是“数学大厦”本身如何建造。至于这座大厦的地基建在哪里，在希尔伯特看来是一件无需考虑的事情。但是，就是这件“无需考虑”的事情，却出现了意想不到的问题。
1901年，年仅29岁的英国哲学家罗素发现了著名的罗素悖论。这一悖论，最简单的表述形式就是所谓的“理发师悖论”。即：小城里的理发师放出豪言：他要为城里人刮胡子，而且一定只要为城里所有“不为自己刮胡子的人”刮胡子。那么，理发师该为自己刮胡子吗？
这一悖论说明了，当时作为“数学大厦”的基础的朴素集合论，在逻辑上是不严谨的。这就是所谓的“第三次数学危机”。为此，数学家们最终将朴素集合论发展成了公理化集合论。更为重要的是，数学家们认识到，不仅数学本身需要公理化，数学基础更需要公理化。
为此，罗素和他在剑桥大学三一学院时的老师、著名哲学家怀特海德，花费了十年时间，完成了三卷本的巨著《数学原理》。
罗素的做法，属于对数学基础进行探究的另外一个学派：“逻辑主义”。这部三卷本的《数学原理》，正是逻辑主义发展的高峰。在《数学原理》中， 数学大厦的一部分被从逻辑出发直接构筑了出来。
这一宏大的目标的代价之一就是推理的极度曲折和冗长。比方说，“1”这个最简单的数字在《数学原理》中直到第363页才被定义；1+1=2这个最简单的小学算术题直到第379页才有结果。
《数学原理》满满两大箱的手稿，被罗素用马车运到了剑桥大学出版社。而出版社对这部巨著的利润估计为：出版这部书会让出版社亏损600英镑。1910年的600英镑，约等于现在的60万元人民币。幸好，剑桥大学出版社并不是纯粹的盈利性出版社，他们愿意为这部学术著作承担300英镑的亏损。剩下的300英镑中，英国皇家学会资助了200英镑。最后这100英镑只得由罗素和怀特海德个人承担。
但是，就在《数学原理》出版之后不久的1931年，年仅25岁的数学家哥德尔证明并发表了两条日后被称作“哥德尔不完备定理”的数学定理。这两条定理表明，包含算术公理的数学体系是不完备的，同时也是不自洽的。
就像开尔文男爵口中的“两朵乌云”彻底改变了物理学大厦的形态一样。哥德尔不完备定理也宣告了，希尔伯特和罗素所希望建立的数学大厦是永远不可能竣工的。
前AI时代的机器证明
虽然希尔伯特和罗素的宏伟计划被哥德尔证明是无法实现的。但是他们的工作，对于数学和计算机的发展，却起到了难以估量的作用。
一方面，这些工作，使得现代数学有了一个相对坚实的基矗另外一方面，这些工作中对公理化和形式化数学的探究，也彻底改变了自古以来数学家们描述数学的语言和研究数学的方式。这一变化最显著的例子就是，现在几乎所有的数学专著，都会选择几乎一模一样的开篇方式。即在开头部分，用集合论之类的语言，给出书中讨论的数学对象的严格定义。
而对希尔伯特公理化三条准则的研究，也催生出现代计算机的理论基矗
哥德尔不完备定理宣告了希尔伯特公理体系中的完备性和自洽性是不成立的。而在同一时期，对于希尔伯特公理体系可决定性的研究也在进行。就在哥德尔发表不完备定理几年后，波兰裔数学家阿尔弗雷德塔斯基和英国数学家阿兰图灵各自独立地证明了，希尔伯特公理体系中的可决定性，也是不成立的。
在证明的过程中，图灵提出了“图灵机”的概念。这一概念，就是现代计算机的理论模型。从本质上讲，包括算盘、机械计算机、电子计算机在内的所有计算“机”，都可以看做是一种具体的图灵机。另外，图灵还证明了，希尔伯特公理体系中的可决定性，和图灵机的停机问题是等价的。
图灵的这些研究，成为日后计算机发展的理论基矗因为在人工智能领域开创性的奠基作用，图灵被称为“人工智能之父”。
二战之后，随着第一代真空管计算机在美国的发展，数学家们也开始尝试在真正的“机器”上去实现那些已有的形式化的数学结论。为了做到这一点，首先需要创造出“机器”能够“听懂”，而且能够用来进行逻辑推理的语言。这时，希尔伯特和罗素所使用的那一套形式化的逻辑符号，也就成为之后发展出的“机器”所使用的各种“数学语言”的基矗
这一时期的主要结果，都是在普林斯顿高等研究院重达2.3吨的真空管计算机“JOHNNIAC”上完成的。1954年，马丁戴维斯开始尝试为JOHNNIAC编写包含自然数和加法的算法程序。他所取得的最大成果就是，让JOHNNIAC证明了“两个偶数的和还是偶数”。
在1956年，同样是在JOHNNIAC上，艾伦纽维尔、赫伯特西蒙和JC肖，用他们开发的程序“逻辑证明机”，证明了罗素的《数学基捶中前52条定理中的38条。对于某些定理，“逻辑证明机”甚至找到了新的、更优雅的证明。
自此，自动化证明（Automated Theorem Proving，ATP）开始逐渐成为一个正式的研究方向。而“逻辑证明机”也被很多人认为是“第一个人工智能程序”。尽管在当时，人工智能这一研究领域还不存在。
在随后的几十年间，自动化证明有了长足的发展。但是，想要真正地让自动化证明产出数学上有价值的结果，还是一件遥遥无期的事情。因为自动化证明，面临一个鱼和熊掌不可兼得的两难局面。能够用来生成有价值的数学结论的证明器通常基于比较强的逻辑系统，而在这类逻辑系统上实现全自动推理还是相当困难的。与之相对的，能够实现强自动化的逻辑系统，如一阶逻辑甚至布尔逻辑，却无法产出真正有价值的数学结论。
面对这一局面，有人工引导的、强逻辑系统下的证明机器成为了发展的主流方向。这也就是所谓的交互式证明（Interactive Theorem Proving，ITP）。
利用交互式证明得出的最早也是最为知名的结果，就是四色定理的证明。
所谓四色定理，用通俗的话来说就是：“每个无外飞地的地图都可以用不多于四种颜色来染色，而且不会有两个邻接的区域颜色相同。”这一问题最早是由南非数学家法兰西斯古德里在1852年提出的，被称为“四色问题”或“四色猜想”。在此后的一百多年时间里，包括闵可夫斯基在内的知名大数学家都研究过这个问题，但是一直没有得到完整的证明。
关于四色定理的证明思路，其实很早就已经明确了。这是因为，地图上相邻国家的接壤方式，可以分为有限多种情况。这些互不相同的情况，被称为构型。所以，只需要逐一验证所有的构型都符合四色定理的情况，就证明了四色定理。但是这一目标的工作量，远远超过了人类能够完成的极限。直到1976年，数学家凯尼斯阿佩尔和沃夫冈哈肯，在美国伊利诺伊大学的IBM 360电脑上，花费了1200小时的时间，验证了所有的1936种构型，从而证明了四色定理。
自那之后，包括双泡猜想、罗宾斯猜想在内的数十个数学问题，以与四色定理类似的方式得到了解决或者取得了重要的进展。
数学家们想要什么？
虽然取得了这些成果，但是交互式的机器证明仍然没有被数学界广泛采用。甚至时至今日，还有数学家在尝试不使用计算机，纯靠人力去证明包括四色定理在内的，这些已经通过机器证明得到解决的数学问题。
这一方面是因为，交互式证明能够解决的问题是有局限性的。而且，交互式证明作为一门独立的研究方向，是有着不低门槛的。它需要掌握相应的人机交互语言。另外，交互式证明主流使用的，以类型论为基础的逻辑体系，也和数学家们习惯的，以集合论为基础的数学体系并不相同。这就导致了如果数学家们想要亲自使用交互式证明，就先要花费不小的学习成本来学习。
更为重要的原因，则是因为数学这门学科本身的价值观。
提起数学，我们的第一反应大概率会是“严格”。在数学里，对就是对，错就是错。在自然数当中1+1永远都只会等于2。数学考试的时候，哪怕最后结果算对了，只要中间步骤有错，也会被老师毫不留情地扣分。
不可否认的是，严格性的确是数学，特别是数学证明中极为重要的价值。但是，只要稍微了解一点儿数学史，以及数学家们的具体工作，我们就难免会产生这样的疑问：严格性是不是数学最重要的价值？
微积分的严格化是由魏尔斯特拉斯完成的。那时距离牛顿和莱布尼茨提出微积分已经过去了快200年。但是这并不影响牛顿和莱布尼兹作为微积分的提出者，被认为是历史上最伟大的数学家之一。也不影响这200年间，数学家们用着不严格的微积分工具，发展出了极为精彩的数学理论和定理。
欧拉的很多极为精彩的工作，以现在的标准来看都是完全不严格的。时至今日，欧拉得出的那个全体自然数的和等于-1/12的结论，还在被各种营销号拿来传播。但是这也丝毫不影响欧拉在数学上的贡献。
黎曼的很多工作是用到的数学理论，例如黎曼映照定理的证明中用到的，椭圆方程的正则性，直到20世纪很晚的时候才逐步建立起来。
直到现在，数学中仍然有很多这样的例子。
对现代几何学的多个领域做出了革命性贡献的俄裔法国数学家格罗莫夫，他的很多论文，按照一般数学工作者的标准来看，已经远远超出了“不严格”的程度。为了理解格罗莫夫的一篇短短十数页的文章中的内容，往往就需要很多数学家去写一系列的文章。
类似的情况还有物理学家出身，却拿下来数学界最高奖菲尔兹奖的爱德华威腾。他的很多工作，都来自于物理学的直觉，而不是数学的严格。
一个数学结果无法被严格写下来，原因可能是多种多样的。一个是数学还没发展到可以用精炼的语言写下严格的论断的时候。牛顿和莱布尼茨、欧拉都是这种情况。在他们的时代，“无穷”还是一个相当模糊的概念，无论是数学上还是哲学上都没有办法准确描述什么是“无穷”。在十九世纪后期这个问题开始被解决之后，人们就能很好地严格化他们的论述。
另一个原因则是出于效率的考虑。即使不谈这些大数学家，作为普通的数学工作者，以及数学专业的学生，在写论文的时候，也不会事无巨细地像机器证明那样写出所有的细节。很多繁琐的内容，都被简简单单的“显然”两个字概括了。
更为主要的原因，则是对于数学理解的考虑。很多数学上的想法，未必是严格的，但很可能是很精彩的。无论是黎曼还是格罗莫夫和威腾，他们写下的“证明”都是充满内涵和启发性的。相较于一个严格的、没有错误的证明，这些“不严格”工作能够让我们对数学的理解更加深入，从而发现更多未知的数学。就像陈省身所说的：“有数学经验和远见的人，能在大海航行下，达到重要的新的领域。”
因此，虽然所有的数学结果，在最后都必须要彻底地严格化。但是在具体的过程中，严格性很多时候其实并不是处在最重要的位置上的。比起一万个严格写下来的形式化的证明，现在数学界主流还是更欣赏一个不严格的但是有深刻内涵的“证明”。
AI是解决之道吗？
那么，现在风头正劲的，以GPT为代表的大型语言模型，能否改变这种局面，让机器证明能够满足数学家们的需求，从而真的变得可用起来呢？
首先，要做到这一点，直接使用诸如GPT这样的通用型的大型语言模型是不行的。
实际上，根据微软研究院对GPT-4的测试报告，数学能力，在GPT-4的各项能力当中，本身就是一个相对的弱项。这很大程度上是因为，GPT的训练和养成，主要是靠互联网上的信息。想要通过这样的方式，获得相当程度的专业数学能力，本身就是不现实的。而且，专业数学能力的培养，本身也不是GPT所要实现的目标。
那么，如果我们换一个思路，将大型语言模型，与已有的交互式证明程序相结合，能不能制造出能够满足数学家们的需求的定理证明机呢？
这种想法是有着很强的合理性的。首先，大型语言模型这一工具，可以让数学家们免去学习使用交互式证明的过程。他们只需要用自己熟悉的语言将问题“告诉”给大型语言模型，然后让模型将其“翻译”给交互式证明程序，完成之后，再将程序给出的形式化的符号结果“翻译”成数学家们习惯的数学语言。
另外，更为重要的是，现在的大型语言模型，已经展现出了一定的逻辑推理能力。按照AI的学习成长速度，再继续发展下去，将来很有可能会出现，能够给出在数学上做出有深刻内涵的启发性工作的人工智能。
本文开头所提到的，由加州理工、英伟达、MIT等机构的学者共同撰写的论文中的工作，就是朝着这个方向迈出的第一步。
他们以Lean，这个由微软研究院的莱昂纳多德莫拉最初于2013年发布的开源交互式证明机为基础，推出了首个基于大型语言模型的开源定理证明机：LeanDojo。
不同于GPT这样“大”型语言模型，LeanDojo要小很多。它的核心数据集，只有96962个定理和证明过程。而且，不同于GPT需要在海量的硬件上进行长时间的训练，LeanDojo的训练过程，只需要单张显卡一周的时间，就可以训练完成。而根据论文中的说法，LeanDojo的数学能力，相较于GPT-4有着显著的提升。
这是因为，相较于泛用型的GPT，专注于数学的LeanDojo，所需要处理的问题要单一得多。而且，形式化数学和机器证明几十年的发展积累，也为LeanDojo的训练提供了一个坚实的基矗
尽管LeanDojo的表现看上去足够让人印象深刻，但是这篇论文的作者们却十分地清醒。他们在论文中写道：这项工作，旨在降低这一领域的进入门槛，并且为今后的工作提供一个可以继续前进的起点。
虽然在现在这个时刻，想要让AI做出数学家级别的工作还远远不可能。但是，大型语言模型和机器证明的结合，至少代表着一种可能性。就像一个小孩在纸上歪歪扭扭地写出了“1+1=2”，所有人的反应，都是会微笑着期待这个小孩将来长大之后会做出什么。
左力
