本文发表于《大众科学》的前博客网络，反映了作者的观点，不一定反映《大众科学》的观点
这是最初发表在美国数学学会联合数学会议博客上的一篇文章的修订版本。
本月早些时候，我参加了在西雅图举行的联合数学会议（JMM）。 我喜欢参加JMM的原因之一是，我可以了解一些我不熟悉的数学领域的最新动态。 今年，我参加了一个名为“数字时代的数学信息”的分会场中的两个讲座，这引发了我对数学家工作内容的思考。
首先，我要坦白：我去参加这个分会场是因为我喜欢橙子。 第一个讲座是托马斯·黑尔斯的讲座，他最出名的可能是他对开普勒猜想的证明。 简而言之，该猜想认为，杂货商堆叠橙子的方式确实是最有效的方式。 这个证明是一个漫长的逐个案例的穷举，而黑尔斯对裁判报告说裁判“99％确定该证明是正确的”并不满意。 因此，他做了任何*数学家都会做的事情：他花了十多年的时间来编写和验证该结果的正式计算机证明。 我参加这个讲座是因为我觉得任何提到开普勒猜想的讲座都有很小的机会为听众准备橙子。
关于支持科学新闻报道
如果您喜欢这篇文章，请考虑通过以下方式支持我们屡获殊荣的新闻报道 订阅。 通过购买订阅，您将帮助确保有关塑造我们当今世界的发现和想法的具有影响力的故事的未来。
黑尔斯的讲座简称为“形式证明”。 这些不是使用呆板的语言编写的证明，也不是写出每个步骤的证明，而是可以输入计算机并一直验证到数学基础（无论选择哪个基础）的证明。
黑尔斯在他的演讲开始时举了一些不太正式的证明的例子，首先是威廉·瑟斯顿的一段话，其中他使用了“细分和抖动”这个短语，这显然不是描述数学的严谨方式。 （顺便说一句，瑟斯顿也用橙子做数学。 他会要求学生剥橙子，以更好地理解二维和三维几何。）
虽然我从未见过瑟斯顿，但我却是他的众多数学后裔之一。 他研究数学的方法，特别是他对直觉和想象力的强调，已经渗透到我扩展的数学家族的文化中，并对我思考数学的方式产生了很大的影响。 这就是为什么对我来说，去参加一个不以直觉为主要重点的讲座是如此令人耳目一新的原因。
黑尔斯当然不是暗示瑟斯顿是一位糟糕的数学家。 瑟斯顿只是他用作不太严谨的数学例子的第一位数学家。 几张幻灯片之后，他提到了关于集合论的布尔巴基著作。 是的，即使是那个形式数学的典范，榨干了每一滴直觉，也并非真正充满了形式证明。
黑尔斯的讲座很好地概述了现有的形式证明程序、一些已被正式证明的数学结果（包括一些已知的结果），以及对该领域未来发展方向的良好介绍。 我对更多地了解QED宣言和FABSTRACTS特别感兴趣，FABSTRACTS是一项将数学论文摘要形式化的服务，这比形式化整篇论文的目标更易于实现。
这次演讲最有趣的时刻，至少对我而言，是听众中有人问及是否可以使用形式证明助手来验证望月新一的abc猜想的证明。 黑尔斯回答说，以目前的技术，您确实需要在输入证明时理解它，因此没有多少人可以做到这一点。 合乎逻辑的回应是：为什么望月新一自己不做呢？ 让我们就说我不抱太大期望。
我参加的本分会场的第二个讲座是迈克尔·舒尔曼的讲座，名为“从nLab到HoTT书籍”。 他谈到了nLab（一个范畴论的维基）和同伦类型论“研究教科书”的写作，这是一本在IAS学期关于同伦类型论（一种替代集合论作为数学基础系统的理论）期间编写的600页巨著。 舒尔曼演讲的主题是“一种尺寸并不适合所有”，无论是在人们协作的方式（对比维基和教科书）还是在数学的基础（类型论与集合论）方面都是如此。
我不知道这是否是故意的，但我认为舒尔曼的演讲是对黑尔斯演讲的一个有趣的对比，对我来说最相关的是它回答了黑尔斯提出的一个问题：为什么没有更多的数学家使用证明助手？ 除了证明助手目前对我们许多人来说过于笨重之外，舒尔曼的回答是，我们进行数学是为了理解，而不仅仅是为了真理。 他说出了我在黑尔斯演讲期间的想法，那就是对于许多数学家来说，使用形式证明助手“感觉不像”数学。 我在这里不是在宣称道德制高点。 实际上，对我来说，能够更快地发现和验证新真理的前景对我来说并没有那么重要，这有点令人惊讶。
你永远不知道当你走进一个远超出你的数学舒适区的讲座时会得到什么。 就我而言，我最终没有得到任何橙子，但我获得了一些关于我们如何以及为何证明的有趣的新视角。
*几乎没有