如果一项数学证明成立，一般意味着它成为了纯粹的客观真理。但是，如果没有人能看懂证明，那对于数学家来说意味着什么？数学家渴求的客观真理能否真正实现？特别是在人工智能迅速发展的今天，相关工具已被用于数学证明，这会对数学本身产生什么样的影响？量子杂志（Quanta Magazine）就这些数学本质问题采访了数论家Andrew Granville，后者认为，数学证明是一种社会契约，而客观性永远无法完全实现。

编译 | 机器之心

Andrew Granville 在蒙特利尔大学校园内。图片来源：Alex Tran/Quanta Magazine2012 年，数学家望月新一（Shinichi Mochizuki）声称已解决了 abc 猜想，这是数论中一个关于加法和乘法关系的难题。但有一个问题：他的证明超过了 500 页，完全晦涩难懂。他的证明依赖于一堆新的定义、符号和理论，几乎所有数学家都觉得无法理解。多年后，有两位数学家将证明的大部分内容翻译为数学家更为熟悉的语言，他们指出了其中的逻辑问题——其中一位数学家称这是「严重且无法修复的漏洞」，而望月新一则以他们未能理解他的工作而拒绝了他们的观点。

这一事件引发了一个基本问题：什么是数学证明？我们倾向于将其视为某种永恒真理的揭示，但也许它更应被理解为一种社会构建。

蒙特利尔大学的数学家 Andrew Granville 最近一直在思考这个问题。一位哲学家读过Granville的文章后联系了他，Granville说：「我开始思考我们是如何得出真理的。一旦你开始探讨这个问题，你会发现这是一个庞大的主题。」

Granville 从小就喜欢算术，但他从未考虑过以数学研究为职业，因为他根本不知道还有这样的行当。他的父亲 14 岁就辍学了，母亲在 15 岁或 16 岁时辍学，他的父母出生在当时伦敦的工人阶级地区，大学教育对他们来说似乎是遥不可及的，所以全家完全不了解学术道路。

在剑桥大学数学专业毕业后，Granville 将 Martin Amis 的小说The Rachel Papers 改编成了电影剧本。在努力推进这个项目，寻求资金支持的过程中，Granville 想找一个不坐办公室的工作——在高中和大学之间的一年间，他曾在一家保险公司工作过，不想再回去了。但他的这部电影并未启动（后来小说被独立拍成电影），Granville 回到学校获得了数学硕士学位，然后搬到加拿大，完成了博士学位。

Granville 直言读博是自己的一次冒险，而且没有抱很大的期望，因为他甚至都不知道什么是博士学位！

但在此后的几十年中，他发表了超过 175 篇论文，大部分是关于数论的。他还因为向大众撰写数学文章而广受欢迎，在 2019 年，他与做编剧的姐姐 Jennifer 合作，共同创作了一本关于素数和相关概念的漫画小说。2023年7月，他的论文How We Arrive at Our Truths被发表在《数学与哲学年刊》（Annals of Mathematics and Philosophy）上。他计划与其他数学家、计算机科学家和哲学家一起，在明年的《美国数学学会公报》（Bulletin of the American Mathematical Society）上发表一系列关于机器如何改变数学的文章。 

量子杂志（Quanta Magazine）与 Granville讨论了数学的本质，为清晰起见，对话经过编辑和缩减。

为什么最近你发表了一篇关于数学证明本质的论文？出发点是什么？

大众媒体通常没有很好地描述数学家是如何进行研究的。人们往往把数学看作是一种纯粹的探索——数学家仅通过纯粹的思想就能得到伟大的真理。但是，数学是关于猜测的——通常是错误的猜测。这是一个试验性的过程，我们在各个阶段中学习。

例如，当黎曼猜想首次出现在 1859 年的一篇论文中时，它就像是魔法一样——突然出现了这么一个惊人的猜想！之后长达 70 年的时间里，人们一直在谈论伟大的思想家仅靠纯思想能做到什么。后来数学家 Carl Siegel 在哥廷根档案馆里发现了黎曼的手稿，黎曼实际上对黎曼函数零点进行了大量计算。Siegel的名言是：「纯粹的思想就到此为止了。」

因此，人们在书写关于做数学的方式上存在某种对立关系，尤其是对于一些哲学家和历史学家，他们似乎认为数学家是一种纯粹的、神奇的生物，是科学的独角兽。但通常情况下并不是这样，纯粹的思维产物其实很少。 

Granville 翻阅着名为“Prime Suspects”的悬疑漫画小说，这是他与他的姐姐合作撰写的，故事以数学为主题。图片来源：Alex Tran/Quanta Magazine如何描述数学家的工作？数学的文化完全是关于证明的。数学家坐在那里思考，所做的 95%的工作都是证明。数学家获得的很多理解都来自于与证明的斗争，以及对这个过程中出现的问题的解释。

大众通常认为证明(proof)是一种数学论证(mathematical argument)，即通过一系列逻辑步骤，论证出一个给定的陈述（命题）是真的。而你论文中提到「这不应该被误解为纯粹的客观真理」，这句话要怎么理解？

证明的主要目的是说服读者相信陈述的真实性，这意味着验证至关重要。我们在数学中拥有最好的验证系统——许多人可以从不同的角度审视证明，而这个过程符合他们所了解和相信的语境。在某种意义上，我们并不是说我们知道它是真的，而是说我们希望它是正确的，因为很多人从不同的角度尝试过。证明是通过这些数学界的标准而被接受的。

然后还有客观性的概念——就是确信所声称的是正确的，感觉自己拥有终极真理，但我们如何知道自己是客观的呢？我们很难将自己从提出陈述的语境中抽离出来，很难拥有社会建立的范式之外的视角。这对于科学思想和其他任何事情都是一样的。

人们还可以问，数学中什么是客观上有趣的或重要的，但这显然也是主观的。为什么我们认为莎士比亚是一位优秀的作家？莎士比亚在他那个时代并不像今天这样受欢迎。显然，关于「什么是有趣的、什么是重要的」存在着社会习惯，这取决于当前的范式。

Granville 继承了其同事的19 世纪的数学著作副本，出版于1811年的 Cribrum Arithméticum，由 Ladislaud Chernac 著，同事在遗嘱中把书留给了他。图片来源：Alex Tran/Quanta Magazine在数学中，范式是什么样的？范式变革的最著名的例子之一就是微积分。当微积分被发明时，它涉及将一个趋近于零的量除以另一个趋近于零的量，导致零除以零，这没有任何意义。最初，牛顿和莱布尼兹提出了无穷小的概念，这让他们的方程式有效。但按照今天的标准来看，这并不合理或严格。

现在，我们有了在 19 世纪末引入的 ε-δ 形式。这种现代表达方式非常绝妙，很好地适用于正确理解这些概念，以至于当你看到旧的表达方式时，你会想，他们当时是怎么想的？而在当时，这被认为是唯一的方法。公平地说，莱布尼兹和牛顿，他们可能会喜欢现代的方法，但受限于那个时代的范式，他们没有想到这样做。所以人们花费了很长时间才得到今天的结果。

问题在于，数学家不知道自己何时处于这种困境中。数学家被困在了自己所创造的社会里，没有外部的视角来说出数学家正在做出什么假设。数学中的一个危险是，你可以认为某些东西不重要，因为它在你选择使用的语言中不容易表达或讨论，但这并不意味着你是对的。

笛卡尔曾经说过，「我认为我了解三角形的一切，但谁能说我真的了解？我是说，未来可能会有人提出一种截然不同的观点，从而更好地理解三角形。」他的这句话是正确的，因为在数学中，你会经常看到这一点。正如你在论文中所写，可以将证明视为一种社会契约（social compact）——一种作者与数学界之间的共识。但已经出现了一个极端的例子，就是望月新一关于 abc 猜想的证明，它没有被接受。

这是个极端的例子，因为望月新一并不想按照通常的方式来给出证明，他选择了模糊不清的方式。当人们取得重大突破，提出全新而复杂的想法时，他们有责任以尽可能易于理解的方式来解释自己的想法，让其他人参与进来。而他更像是说，如果你不想按照我写的方式来读它，那不是我的问题。他有权按照自己想要的方式来做研究，但这与数学界无关，与数学家取得进展的方式无关。

「我们继续努力证明我们能证明的东西，」 Granville 说。图片来源：Alex Tran/Quanta Magazine如果证明存在于社会语境中，那么它们如何随着时间的推移而改变？

一切都始于亚里士多德，他说需要有某种演绎系统。你只能通过基于你已知并确定的东西来证明新事物，回溯到某些 「原始命题」或公理。所以问题是：你知道的哪些基本的事情是正确的？很长一段时间以来，人们只是说，线是线，圆是圆；有一些简单明了的事物，应该以这些假设为出发点。

这种观点已经存在了很长时间，在很大程度上至今仍然存在。但是发展起来的欧几里得公理系统：「一条线就是一条线」，也有它的问题。基于集合概念，伯特兰・罗素（Bertrand Russell）发现了一些悖论。此外，人们可以在数学语言中玩文字游戏，创建有问题的命题，如「这个命题是假的」（如果它是真的，那么它是假的；如果它是假的，那么它是真的），这表明了公理系统存在问题。

所以，罗素和阿尔弗雷德・怀特海（Alfred Whitehead）试图创建一种可以避免所有这些问题的新数学系统。但这个系统复杂过头了，很难相信他们的基础元素是正确的，没有人对此感到满意。像证明 2+2=4 这样的事情，从出发点开始需要大量的内容，这样的系统有何意义？

然后大卫·希尔伯特（David Hilbert）出现了，有了这个了不起的想法：也许我们根本不应该告诉人们要从什么是完全正确的事物开始。相反，任何有效、简单、连贯、一致的出发点，都值得探讨。你不能从你的公理中演绎出互相矛盾的两个事物，而且你应该能够用所选的公理来描述大多数数学。但你不应该先验地说这是什么。

这似乎也符合我们之前关于数学中客观真理的讨论。20 世纪初，数学家们开始意识到可能存在多种公理系统：一个给定的公理集不应被视为普遍原则或不言而喻的真理？

是的。希尔伯特开始并不是出于抽象的原因而这样做的。他对不同的几何概念非常感兴趣，比如非欧几何。这引起了很大争议。那时人们会问，如果你给我这样一个「线」的定义——它可以绕过盒子的角，那我为什么要听你的？希尔伯特说，如果他能够使其有条理并保持一致，你就应该听，因为这可能是我们需要理解的另一种几何学。这种观点的变化——允许使用任何公理系统——不仅适用于几何学，它适用于所有数学。

当然，有些东西比其他东西更有用。所以我们大多数人都使用相同的 10 个公理，这个系统叫作 ZFC，即策梅洛—弗兰克尔集合论 （Zermelo-Fraenkel Set Theory，含选择公理时常简写为 ZFC，C代表选择）。

这就引出了一个问题，什么可以从中演绎出来，什么不能。有一些命题，比如连续统假设，不能使用 ZFC 来证明假设是成立的，必须引入新的公理，你可以选择自己的公理系统，当然也可以选择其他公理来证明其不成立。这相当酷，我们应继续保持多样性。根据库尔特·哥德尔（Kurt Gödel）的说法，我们仍然需要基于品味来做选择，而且希望我们有好的品味。数学家应该做有道理的事情，而且他们也确实这样做了。提到哥德尔，他对数学公理系统也是相当重要的角色。

要讨论数学，你需要一种语言，以及在这种语言中遵循的规则。在 20 世纪 30 年代，哥德尔证明，无论你选择哪种语言，总会有在这种语言中陈述为真的内容，但它不能从你的起始公理中被证明。实际上更为复杂，并且你会陷入这个哲学困境：如果你不能证明它，那什么才是一个真实的陈述？这是一个大麻烦，我们能做的是有限的。专业数学家在很大程度上忽视了这一点。数学家专注于可行的事情。正如彼得·萨纳克（Peter Sarnak）经常说的那样，「我们是工作的人。」数学家继续努力证明其所能证明的东西。

「数学中的一个危险是，你可以认为某些东西不重要，因为它在你选择使用的语言中不容易表达或讨论，但这并不意味着你是对的。」 Granville 说。

目前不仅仅是计算机，甚至人工智能，都应用到数学，那么证明的概念正在发生变化吗？我们现在已经进入了一个不同的领域，计算机可以做一些不同寻常的事情。现在人们说，哦，我们有这台计算机，它可以做人类无法做到的事情。但它真的可以吗？它真的可以做人类无法做到的事情吗？早在 1950 年代，艾伦・图灵（Alan Turing）说过，计算机被设计用来做人类可以做的事情，只是更快而已。

数十年来，数学家一直在使用计算机，比如进行有助于他们理解理论的计算。人工智能可以做的新工作是验证我们认为是真实的东西。我们已经在证明验证方面取得了一些令人振奋的进展，比如 Lean（证明助手），数学家能够通过它验证许多证明，同时它也帮助作者更好地理解他们自己的工作，因为他们必须将一些想法分解成更简单的步骤，以供 Lean 进行验证。

但这是百分之百可靠的吗？只要 Lean 同意它是一个证明，那么它就是一个证明吗？在某些方面，这取决于将证明转化为 Lean 输入的人的能力。这听起来很像做传统数学的方式。不是说像 Lean 这样的东西会产生很多错误，只是不确定它是否比大多数人类做的事情更可靠。

计算机可以成为正确完成任务的非常有价值的工具，特别是对于验证严重依赖新定义的数学内容，而这些定义乍一看并不容易分析。毫无疑问，在我们的「武器库」中拥有新的观点、新的工具和新的技术是很有帮助的。但我回避的是以下这种概念：我们现在将拥有能够产生正确定理的完美逻辑机器。

必须承认，数学家不能确定计算机的结果是否正确。数学的未来必须依赖于整个科学历史上一直依赖的科学界的理解：不断证伪，与那些从完全不同角度看同一问题的人交流，等等。

随着这些技术变得更加复杂，未来会变成什么样？

也许它可以帮助创造一个证明。可能五年后，我们对像 ChatGPT 这样的人工智能模型说，「我很确定我在某个地方看到过这个问题。你能检查一下吗？」它可能会回复一个相似陈述，并且是正确的。一旦它变得非常擅长这一点，也许你可以再进一步说，「我不知道怎么做这个，有没有人做过类似的事情？」也许最终，一个人工智能模型可以找到搜索文献的熟练方法，把已经在其他地方使用过的工具运用到新的问题上。这是一个数学家可能无法预见的方式。

但是，我不知道 ChatGPT 会如何超越某种层次，以超越数学家的方式来证明。ChatGPT 和其他机器学习程序并不能思考，它们是基于许多示例的词汇联想。因此，它们似乎不太可能超越它们的训练数据。但如果发生这种情况，数学家将怎么办呢？数学家所做的许多事情都是为了证明。如果你从数学家这里拿走了证明，那么数学家会成为什么样子呢？ 

无论如何，当我们想运用计算机进行辅助工作时，我们需要考虑所有从人类在努力发展中学到的教训：使用不同的语言、共同工作、持有不同的观点的重要性。不同社群聚集在一起共同研究和理解一个证明，呈现出一种稳健性，这才是健康的。如果我们要在数学中使用计算机辅助，我们也需要以同样的方式将其丰富起来。

本文转载自“机器之心”，编辑：rome rome，《返朴》对译文进行了重新修订

原文链接：https://www.quantamagazine.org/why-mathematical-proof-is-a-social-compact-20230831/。