证明助手跳到大联盟数学

多年来，计算机证明助手一直是数学中一个有趣的子情节——承诺将数学家工作方式的核心方面自动化，但在实践中对该领域几乎没有影响。但 6 月初完成的一个新结果，有种菜鸟在大联盟中首创的感觉：终于，一位证明助手通过验证复杂的现代数学的正确性，为数学研究的前沿做出了真正的贡献。证明。 “这表明现代数学可以在定理证明器中形式化，”剑桥大学研究生 Bhavik Mehta 说，他为这项工作做出了贡献。有问题的证明是由波恩大学的 Peter Scholze 提出的，他是世界上最受尊敬的数学家之一。这只是他和哥本哈根大学的达斯汀·克劳森 (Dustin Clausen) 多年来一直致力于的名为“浓缩数学”的更大项目的一部分。他们的目标是为拓扑创建新的基础，用作者称之为凝聚集的更通用的对象取代拓扑空间的传统概念——其例子包括球体和甜甜圈。在这个新视角中，拓扑空间被认为是由无数粘在一起的尘埃点组装而成的。该项目包括一个特别重要且困难的证明，证明 Scholze 在 2019 年 7 月的一个消耗周中自己计算出来。它表明，如果用压缩集替换拓扑空间，称为实函数分析的数学领域仍然有效。 Scholze 在星期一开始了证明。他完全在头脑中工作，几乎没有写下任何东西，更不用说使用电脑了。到周四下午，他几乎已经想通了，只留下了一件他做不对的事。他也感受到了在他活跃的记忆中保持如此复杂的争论所需的高度集中的压力。所以那天晚上他和一些朋友在酒吧放松了。第二天早上，星期五，他付了钱。

但他也知道他周末没有时间工作，这让周五成为完成证明的最佳机会。想到要与过去一周他在脑海中建立的一切失去联系，然后不得不在周一重新开始，这超出了他的考虑。 “我不认为我有能力在脑海中再次重建它，”Scholze 说。于是他通电并完成了证明。但事后，他并不确定自己所做的是否正确。原因不仅仅是他清除了最后一道障碍的朦胧环境。证明是如此复杂 Scholze 知道他可能漏掉了一些东西。 “这是一件非常复杂的事情，有许多活动部件。当您改变这些参数之一时，很难知道哪些部件移动了多少，”Scholze 说。直到 2019 年 11 月，Scholze 才抽出时间真正写下证明。一年后，他联系了伦敦帝国理工学院的数学家 Kevin Buzzard，他也是一个名为 Lean 的证明助理项目的著名传播者。 Scholze 想知道是否有可能将他的证明输入到 Lean 中——把它像软件程序一样变成代码行——这样程序就可以验证它是否真的正确。 Buzzard 与包括弗莱堡大学博士后研究员 Johan Commelin 在内的少数精益社区成员分享了 Scholze 的调查。 Commelin 拥有适合这份工作的完美背景——他已经使用 Lean 多年并且熟悉压缩数学——并且他相信验证 Scholze 的证明对于证明助理在数学界的地位合法化有很大帮助。 “能够在这样一个项目上与彼得合作并附上他的名字对精益来说将是一个巨大的推动，”Commelin 说。

但他也认为这可能需要一年或更长时间才能完成，这让他犹豫了。 Commelin 担心他可能会花费所有时间来验证证明，最后，数学界的其他人只会耸耸肩。 “我想，如果我花两年时间研究这个，然后走出我的洞穴说，‘这很好’，世界其他地方会说，‘哇，我们已经知道了，彼得证明了这一点， ’”科梅林说。 Scholze 本人并不完全确定，这并不重要。因此，Commelin 问 Scholze，他是否愿意发表公开声明，证明这项工作的重要性。 Scholze 同意了，并于 2020 年 12 月 5 日在 Buzzard 的博客上写了一篇文章。他们将其称为“液体张量实验”，这是对称为液体实向量空间的证明中涉及的数学对象的一种致敬，并向他和 Commelin 喜欢的前卫摇滚乐队致敬，称为液体张力实验。在 4,400 字的初级读物中，Scholze 解释了结果的一些技术方面，然后添加了一个注释，用通俗的语言证明他认为用计算机检查它的重要性。 “我认为这可能是我迄今为止最重要的定理。 （到目前为止，它还没有真正的应用程序，但我相信这会改变，）”Scholze 写道。 “最好确保它是正确的……” 保证到位，Commelin 开始工作。在向 Lean 解释了他最终希望程序检查其证明的数学陈述之后，他将更多的数学家带入了该项目。他们确定了一些引理——证明中的中间步骤——看起来最容易上手。他们首先将这些形式化，在精益用来确定给定陈述是否正确的数学知识库之上对它们进行编码。去年 10 月，广达写道，用精益编写数学的集体努力具有“提高谷仓的气氛”。这个项目也不例外。 Commelin 将识别证明的离散部分并将它们发布到 Zulip，一个作为精益社区中心的讨论板。当数学家看到适合他们专业知识的部分证明时，他们会自愿将其形式化。

Mehta 是为这项工作做出贡献的十几位数学家之一。 5 月，他看到了 Commelin 的一篇帖子，请求帮助将一个名为 Gordan 引理的陈述的证明形式化，该陈述与 Mehta 在组合几何领域的工作有关。他花了一周时间用与数学家正在构建的更大的证明一致的术语对证明进行编码。他说，这是精益工作方式的象征。 “这是一次大型合作，很多人都在做他们擅长的事情来制作一个单一的整体，”他说。随着工作的进行，Scholze 始终如一地出现在 Zulip 上，回答问题并解释证明要点——有点像建筑师在工作现场为建筑商提供指导。 “他总是触手可及，”科梅林说。 5 月底，该小组完成了 Scholze 最不确定的证明的一部分。 5 月 29 日凌晨 1 点 10 分，Commelin 输入了最后的击键。Lean 编译了证明，它像一个正常运行的程序一样运行，验证 Scholze 的工作是 100% 正确的。现在 Scholze 和其他数学家可以将这些技术从真正的泛函分析应用到压缩集，因为他们知道他们肯定会在这个新环境中工作。虽然 Scholze 仍然喜欢在脑海中找出证据，但 Lean 的能力给他留下了深刻的印象。他现在可以预见像它这样的程序在研究数学中发挥持久的作用。 “这个实验彻底改变了我对 [证明助理] 能力的印象，”Scholze 说。 “我现在认为原则上在精益中将您想要的任何内容形式化是明智的。没有真正的障碍。”