本文发表于《大众科学》的前博客网络，反映了作者的观点，不一定反映《大众科学》的观点
在我的上一篇专栏文章中 我叙述了在1990年代，两位数学家如何以我的名字命名一个几何对象“霍根曲面”，以报复我的“证明的消亡”。这篇专栏文章给了我一个机会，重新审视我1993年那篇有争议的文章，该文章认为计算机的进步、数学日益增长的复杂性以及其他趋势正在削弱传统证明的地位。在撰写专栏文章时，我意识到霍根曲面产生的证明与我的“证明消亡”论题相矛盾。我给几位专家发了电子邮件，询问他们认为我的“证明消亡”论题的现状如何。以下是计算机科学家斯科特·阿伦森、数学物理学家彼得·沃伊特和数学软件巨头斯蒂芬·沃尔夫勒姆的回复。（有关我与他们的问答链接，请参阅“延伸阅读”）。如果/当他们有更多评论时，我会添加更多评论。 –约翰·霍根
斯科特·阿伦森的回应（他也刚刚发布在他的博客上）：
约翰，我喜欢你，所以我很不愿意这么说，但过去四分之一个世纪对你关于“证明消亡”的论题并不友好！ 那些给你发愤怒信件的数学家们说得有道理：数学界并没有发生任何值得如此戏剧性标题的根本性变化。 基于证明的数学仍然非常健康，例如，自从你的文章发表以来，庞加莱猜想得到了解决，埃尔德什差异问题、卡迪森-辛格猜想、卡塔兰猜想、素数中的有界间隙、确定性多项式时间内的素性测试等等——仅仅从我略知一二的极小部分领域中挑选了一些例子。
关于支持科学新闻业
如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻业 订阅。通过购买订阅，您正在帮助确保有关塑造我们当今世界的发现和思想的具有影响力的故事的未来。
数学实践中存在着演变性的变化，就像一直以来那样。 自2009年以来，网站MathOverflow让数学家可以就一个晦涩的参考文献或证明中一个顽固的步骤查询全球集体智慧，并获得近乎即时的答案。 同时，“多数学者”项目也取得了一定的成功，他们试图利用博客和其他社交媒体，通过大规模协作来推进长期存在的未解决数学问题。
虽然人类仍然坐在驾驶座上，但人们一直在努力增加计算机的作用，并取得了一些显著的成功。 这些成功包括托马斯·黑尔斯在1998年对开普勒猜想（关于橙子最密集的堆积方式）的计算机辅助证明——现在已经从头到尾完全通过机器验证，《数学年刊》拒绝发表传统数学和计算机代码的混合物之后。 它还包括威廉·麦丘恩在1996年对代数中的罗宾斯猜想的解决方案（计算机生成的证明只有半页，但涉及的替换非常奇怪，以至于60年来没有人发现它们）；以及“另一个极端”，2016年由马林·休勒和合作者对布尔毕达哥拉斯三元组问题的解决方案，其大小为200太字节（当时是“数学史上最长的证明”）。
有一天，计算机可能会取代人类在数学研究的所有方面——但也有可能，当它们能够做到这一点时，它们也将能够取代人类在音乐、科学新闻和所有其他领域的工作！
新的证明概念 ——包括概率证明、交互式证明、零知识证明，甚至量子证明——自1993年以来在理论计算机科学家中得到了进一步发展。 然而，到目前为止，这些新型证明仍然要么完全是理论性的（如量子证明），要么用于密码协议，而不是用于数学研究。 （例如，零知识证明现在在某些加密货币中发挥着重要作用，例如Zcash。）
在许多数学领域（包括我自己的理论计算机科学），证明变得越来越长，任何一个人都难以理解。 这导致一些人提倡一种分离方法，即人类数学家只相互讨论模糊的直觉和高层次的概念，而繁琐的细节验证则留给计算机。 然而，到目前为止，以机器可检查的格式编写证明所需的大量时间投入——几乎没有新的见解回报——阻止了这种方法的广泛采用。
是的，数学中存在非严格的方法，这些方法继续在物理学、工程学和其他领域广泛使用，就像一直以来那样。 但是，只要有严格的证明可用，这些方法都没有取代证明作为黄金标准的地位。 如果我不得不推测原因，我会说：如果你使用非严格的方法，那么即使你清楚在什么条件下你的结果可以被信任，其他人也可能不太清楚。 此外，即使研究社区中只有一部分人关心严谨性，该部分人所依赖的任何早期工作也需要是严格的——从而在该方向上施加持续的压力。 因此，给定的研究领域变得越协作，严谨性就越重要。
在我看来，一个世纪前，康托尔、弗雷格、皮亚诺、希尔伯特、罗素、策梅洛、哥德尔、图灵等人在数学基础方面的阐明，仍然是人类思想最伟大的成就之一，与进化论、量子力学或任何其他事物并驾齐驱。 诚然，这些伟人设定的理想仍然主要是理想化的。 当数学家说一个定理已被“证明”时，他们的意思仍然像以往一样，更像是：“我们已经达成社会共识，所有思路都已到位，可以进行严格的形式证明，该证明可以由机器验证……剩下的唯一任务是大量的死记硬背编码工作，我们没有人打算永远做下去！” 同样真实的是，数学家作为人类，会受到你可能期望的各种弱点的影响：声称已经证明了他们没有证明的东西，为谁证明了什么而争吵，指责他人缺乏严谨性，同时自己却虚伪地放纵。 但正如爱和诚实仍然是美好的理想，无论它们被违反多少次一样，数学的严谨性也是如此。
彼得·沃伊特的回应
回想四分之一个世纪前的这场辩论，最让我震惊的是变化如此之小。 现在有很多资金和注意力都集中在数据科学、机器学习、人工智能等方面，但除了更多的学生在这些领域找到工作之外，对纯数学研究的影响微乎其微。 一个变化是互联网提供了更好的访问高质量数学研究材料和讨论的途径，例如讲座视频、MathOverflow上的讨论以及我的同事约翰·德容的Stacks Project。 这种变化使人们像以往一样进行交流，只是更有效率。
与此同时，计算机在数学定理的证明的创建和检查中仍然很少发挥作用。 围绕望月新一宣称证明abc猜想的激烈辩论提供了一个有趣的案例。 理解和检查证明的问题涉及到该领域最优秀的人才，他们正在为理解而进行艰难的斗争，而计算机化的证明检查根本没有发挥任何作用。 没有证据表明计算机软件现在比1993年更接近与彼得·舒尔茨和其他专家竞争，这些专家致力于分析望月新一的论证。 如果这个故事未来有新的积极发展，那将是来自有血有肉的数学家，而不是科技行业的服务器农场，在更深入的理解方面取得进展。
斯蒂芬·沃尔夫勒姆的回应。 当我联系Mathematica和其他产品的创始人沃尔夫勒姆时，一位公关人员发给我一个链接，指向沃尔夫勒姆最近的文章“逻辑、可解释性和理解的未来”。这篇文章充满了关于数学、逻辑、证明、计算和一般知识本质的挑衅性断言。沃尔夫勒姆首先声称，他已经绘制出了所有可能逻辑公理的空间，他认为，这表明我们通常依赖的公理并非以某种方式是最优或必要的，而是任意的。我的理解是，可能的数学空间虽然是无限的，但可能比通常认为的更无限。沃尔夫勒姆还暗示，借助他的一项发明Wolfram Language，计算机证明不必是黑匣子，它们生成结果，但几乎不产生理解。以下是他对此的看法：
在某种程度上，我认为将证明通常呈现给人类理解，而程序通常只被认为是供计算机运行的东西，这是一种历史的怪癖……[O]我在过去几十年努力的主要目标之一是改变这种状况——并在Wolfram Language中开发一种真正的“计算通信语言”，在这种语言中，计算思想可以用一种计算机和人类都容易理解的方式进行交流。
但沃尔夫勒姆警告说，我们永远会遇到理解的极限
在数学中，我们习惯于构建我们的知识堆栈，以便每个步骤都是我们可以理解的。但实验数学——以及诸如自动定理证明之类的事物——清楚地表明，有些地方是我们无法具备这种特征的。我们会称之为“数学”吗？我认为我们应该称之为“数学”。但这与我们过去一千年主要使用的传统不同。这是一个我们仍然可以构建抽象，并且仍然可以构建新的理解水平的传统。但在这之下的某个地方，将存在各种各样的计算不可约性，我们将永远无法真正将其带入人类理解的领域。
卡尔·达尔克的回应： 达尔克是一位数学家，我之前曾与他通信。请访问他的网站这里。
科学的终结（你最喜欢的话题之一）和形式证明的终结之间可能存在相似之处。两者都可以更准确地改述为不可避免的收益递减规律。我们不期望在这些领域中的任何一个领域发生范式转变，尽管渐进式进步始终是可能的，但其实现的成本却越来越高。数学和科学的低垂果实在文艺复兴时期被采摘，到1960年，中间的树枝也被剥光了。 为了到达树冠，我们动用计算机，就像用高空作业车将我们送到树的更高处一样，但这项技术帮助了我们，它并没有取代我们。人仍然必须用手摘水果， 而且我不希望这种情况在短期内发生改变。
在粒子物理学中，证实希格斯玻色子的超大型强子对撞机可能是有史以来建造的最大机器，但 人类必须解释数据；对撞机本身并没有发现任何东西。同样，计算机帮助数学家进行研究，但我们必须自己构建形式证明。你提到了大卫·霍夫曼曲面，计算机提供了直觉，但数学家编写了证明。
“实验几何实验室”是另一个例子。比尔·戈德曼部分说道：“尝试解释数学的练习……实际上帮助我们发现了新的结果，即使计算机本身在发现过程中并没有真正发挥太多作用。对计算机进行编程以生成几何图像所需的细节程度可以提高研究人员对游戏中思想的理解。”
除了计算机之外，合作也是关键，通常是在国际范围内。成千上万的科学家和工程师共同努力证实了希格斯玻色子，同样地，数百名数学家合作证明了费马大定理。安德鲁·怀尔斯获得了荣誉，他的贡献不应被低估，但他站在巨人的肩膀上。即使在计算机的帮助下，一个人的大脑也几乎无法容纳，更不用说创造，一个现代证明。这个Nova特辑列出了使怀尔斯证明成为可能的所有数学家；跳转到结尾并观看它滚动播放。 http://www.pbs.org/wgbh/nova/proof/wiles.html
所有这一切都对研究生产生了影响，正如我在1990年发现的那样。我的学术顾问告诉我，在伯克利获得博士学位的平均时间是7.5年。我感到茫然。我愿意花费十分之一的生命来获得博士学位吗？而我的储蓄账户正在减少，我妻子的生物钟也在滴答作响？事实证明，我不愿意；我获得了硕士学位，找到了一份程序员的工作，并组建了家庭。博士学位的标准是，而且一直都是，原创研究，带有“有趣的”原创研究的潜台词，由该领域的专家判断。然而，新的成果越来越难获得。
这在纯数学中尤其如此，但也可能适用于其他领域。在某个时候，博士学位的标准可能不得不转变——也许是对正在进行的研究的贡献，即使它尚未产生任何成果，或者可能是为了清晰或教育目的而对现有材料进行重新包装，就像乐队翻唱一首已有的歌曲一样。我无法预测这将走向何方，但很少有研究生可以将他们生命中的8年或10年投入到博士课程中，寻找太阳下的新事物，同时他们还要兼职以维持生计。
延伸阅读:
身心问题 （免费在线书籍）