2023/10/04 20:57

数学家孜孜以求的数学证明本质是一种社会契约，为什么这么说？

数学的本质是什么？数学家渴求的客观性真理是否能实现？人工智能等的发展和在数学中的应用会对数学产生什么样的影响？本文中数论学家 Andrew Granville 探讨了数学的真正本质以及为什么客观性永远无法完全实现。

^{Andrew Granville 在蒙特利尔大学校园内。}

2012 年，数学家望月新一声称已解决了 abc 猜想，这是数论中一个关于加法和乘法关系的难题。但有一个问题：他的证明超过了 500 页，完全晦涩难懂。论文依赖于一堆新的定义、符号和理论，几乎所有的数学家都觉得无法理解。多年后，当两位数学家将证明的大部分内容翻译成更为熟悉的数学语言时，他们指出了被其中一位数学家称之为「严重且无法修复的漏洞」的逻辑问题，而望月新一则以他们未能理解他的工作而拒绝了他们的观点。

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

蒙特利尔大学数学家 Andrew Granville 最近一直在思考这个问题。在一位哲学家联系他讨论关于他的一些写作后，他说：「我开始思考我们如何得出自己的真理。一旦你开始探讨这个问题，你会发现这是一个广泛的主题。」

Granville 从小就喜欢算术，但他从未考虑过从事数学研究的职业。他的父亲 14 岁就辍学了，母亲在 15 或 16 岁时辍学，他的父母出生在伦敦当时的工人阶级区域，大学教育对他们来说似乎是遥不可及的。所以当时全家对数学一点都不了解。

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

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

但在此后的几十年中，他发表了 175 多篇论文，大部分是关于数论的。他还因为向广大读者撰写数学文章而广受欢迎，在 2019 年，他与做编辑的姐姐 Jennifer 合作，共同创作了一本关于素数和相关概念的图书。上个月，他的论文《How We Arrive at Our Truths》被发表在《数学与哲学年刊》上。与其他数学家、计算机科学家和哲学家一起，他计划在明年的《美国数学学会通报》上发表一系列关于机器如何改变数学的文章。

下面量子杂志对与 Granville 的对话进行了一番整理。

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

Granville 回答道，数学家进行研究的方式通常很难讨好大众媒体。人们往往把数学看作是一种纯粹的追求，其实数学家只是通过纯思维来得出伟大的真理。但数学是关于猜测的 —— 通常是错误的猜测。这是一个实验性的过程。

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

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

^{Granville 翻阅着一本名为《Prime Suspects》的图书小说，这本小说是他与他的姐姐合作撰写的，故事以数学为主题。}

如何描述数学家所做的工作？

数学的文化完全是关于证明的。数学家坐在那里思考，所做的 95% 都是证明。他们获得的很多理解都来自于努力证明和解释在努力证明时出现的问题。

大众通常认为证明是一种数学论证。通过一系列逻辑步骤，它证明了一个给定的陈述是真实的。对于论文中提到「这不应该被误解为纯粹的客观真理」，这句话要怎么理解？

证明的主要目的是说服读者陈述的真实性，这意味着验证至关重要。数学拥有的最好的验证系统是许多人从不同的角度看待证明，而且它在他们知道和相信的背景下很合理。在某种意义上，我们并不是在说我们知道它是真的。我们在说我们希望它是正确的，因为很多人从不同的角度尝试过。证明是通过这些数学家团体的标准来接受的。

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

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

^{Granville 继承了其同事的这本 19 世纪的数学著作，《The 1811 Cribrum Arithméticum》由 Ladislaud Chernac 著。}

在数学中，这是什么样的呢？

范式变革的最著名例子之一就是微积分。当微积分被发明时，它涉及将一个趋近于零的量除以另一个趋近于零的量，导致零除以零，这没有任何意义。最初，牛顿和莱布尼兹提出了无穷小的概念。这让他们的方程式有效，但按照今天的标准来看，这并不合理或严格。

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

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

笛卡尔曾经说过，「我认为我对三角形了解一切，但谁能说我真的了解？我是说，未来可能会有人提出一种截然不同的视角，从而更好地理解三角形。」他的这句话是正确的，因为在数学中，你很会经常看到这一点。

论文中有提及可以将证明视为一种社会契约，一种作者与数学界之间的共识。已经出现一个极端的例子，这种方法不起作用，就是望月新一关于 abc 猜想的证明。

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

^{「我们继续努力证明我们能证明的东西，」 Granville 说。}

如果证明存在于社会背景中，那么它们如何随着时间的推移而改变？

一切都始于亚里士多德，他说需要有某种演绎系统。你只能通过基于你已知并确定的东西来证明新事物，回溯到某些 “原始命题」或公理。

所以问题是：那些你知道是真实的基本事物是什么？很长一段时间以来，人们只是说，线是线，圆是圆；有一些简单明了的事物，那些应该是我们出发点的假设。

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

所以，罗素和阿尔弗雷德・怀特海德试图创建一种可以避免所有这些问题的新数学系统。但这个系统非常复杂，很难相信这些是正确的出发点。没有人对此感到满意。像证明 2+2=4 这样的事情从出发点需要大量的空间。这样的系统有何意义？

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

20 世纪初，数学家们开始意识到可能存在多种公理系统：一个给定的公理系统不应被视为普遍或不言而喻的真理？

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

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

这就引出了什么可以从中演绎出来，什么不能的问题。有一些陈述，比如连续性假设，不能使用 ZFC 来证明。必须有第 11 个公理，而且你能以两种方式解决它，因为你可以选择自己的公理系统。这相当酷。我们继续保持多样性。不清楚什么是对的，什么是错的。根据库尔特・哥德尔的说法，我们仍然需要基于品味来做选择，而且我们希望我们有好的品味。数学家应该做有道理的事情，而且他们也确实这样做了。

哥德尔对数学公理系统也是相当重要的角色

要讨论数学，你需要一种语言和在这种语言中遵循的一组规则。在 20 世纪 30 年代，哥德尔证明，无论你如何选择你的语言，总会有在那种语言中为真但不能从你的起始公理中证明的陈述。实际上比这更复杂，但仍然存在这个哲学困境：如果你不能证明它，那什么才是一个真实的陈述？

这是一个大麻烦，我们在自身所能做的方面有限。专业数学家在很大程度上忽视了这一点。数学家专注于可行的事情。正如彼得・萨纳克经常说的那样，「我们是工作的人。」数学家继续努力证明其所能证明的东西。

^{「数学中的一个危险是，你可以将某事看作不重要，因为它在你选择使用的语言中不容易表达或讨论。这并不意味着你是对的，」 Granville 说。}

目前不仅仅是计算机，甚至人工智能，都应用到数学，那么证明的概念正在发生变化吗？

现在已经进入了一个不同的领域，计算机可以做一些不同寻常的事情。现在人们说，哦，我们有这台计算机，它可以做人类无法做到的事情。但它真的可以吗？它真的可以做人类无法做到的事情吗？早在 1950 年代，艾伦・图灵说过，计算机被设计用来做人类可以做的事情，只是更快而已。并没有太多改变。

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

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

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

必须承认，数学家不能确定计算机的结果是正确的。数学的未来必须依赖于整个科学历史上一直依赖的科学社群的意识：互相交流意见，与那些从完全不同角度看同一问题的人交谈，等等。

未来随着这些技术变得更加复杂，它们会发展到何种程度？

也许它可以帮助创建一个证明。可能若干年后，我们对像 ChatGPT 这样的人工智能模型说「我很确定我在某个地方看到过这个问题。你能检查一下吗？」，它可能会回复一个相似但正确的陈述。

然后，一旦它变得非常擅长这一点，也许你可以再进一步说「我不知道怎么做这个，但有没有人做过类似的事情」。也许最终，一个人工智能模型可以找到搜索文献的熟练方法，以运用已经在其他地方使用过的工具。这是一个数学家可能无法预见的方式。

但是 ChatGPT 如何在超越数学家的情况下进行证明，这个让人比较难理解。ChatGPT 和其他机器学习程序并没有思考，它们是基于许多示例的词汇联想。因此，它们似乎不太可能超越它们的训练数据。但如果发生这种情况，数学家将怎么办呢？数学家所做的许多事情都是证明。如果你从数学家这里拿走了证明，那么数学家会成为什么样子呢？

无论如何，当我们考虑将计算机辅助应用到哪里时，我们需要考虑从人类努力中学到的所有教训：使用不同的语言、共同工作、持有不同的观点的重要性。不同社群聚集在一起共同研究和理解一个证明时，呈现出健壮性、健康性。如果数学家要在数学中使用计算机辅助，需要以同样的方式丰富它。

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

理论Andrew Granville