小乐数学科普证明助手Lean大显身手验证数学定理量子杂志

　　作者：Kevin Hartnett 2021-7-28 译者：zzllrr小乐 2021-7-29
　　多年来，计算机证明助手一直是数学中一个有趣的次要情节——有望将数学家核心工作方式自动化，但在实践中对该领域几乎没有影响。
　　但 6 月初完成的一个新结果，有一种某个菜鸟在大联盟中崭露头角的感觉：终于，一个证明助手通过验证一个复杂的现代证明的正确性，为数学研究的前沿做出了真正的贡献。
　　＂它表明现代数学可以在定理证明器中形式化，＂剑桥大学研究生 Bhavik Mehta 说，他为这项工作做出了贡献。
　　问题证明是由波恩大学的 Peter Scholze (彼得·舒尔茨)提出的，他是世界上最受尊敬的数学家之一。这只是他和哥本哈根大学的Dustin Clausen (达斯汀·克劳森) 多年来一直致力于的名为＂凝聚数学＂（condensed mathematics）的更大项目的一部分。
　　他们的目标是为拓扑学创建新的基础，用作者称之为凝聚集（condensed mathematics）的更通用的对象取代拓扑空间的传统概念（拓扑空间例如：球体和甜甜圈）。在这个新视角中，拓扑空间被认为是由无数粘在一起的尘埃点组装而成的。
　　该项目包括一个特别重要且困难的证明，由Scholze 在 2019 年 7 月的一个星期自己费力证明出来。它确定，如果你用＂凝聚集＂替换拓扑空间，称为实泛函分析的数学领域仍然有效。
　　Scholze 在星期一开始了证明。他完全在大脑中工作，几乎没有写下任何东西，更不用说使用电脑了。到周四下午，他几乎已经想通了，只留下了一件他做不对的事。他也感受到了在他活跃的记忆中保持如此复杂的论点所需的高度集中的压力。所以那天晚上他和一些朋友在酒吧放松了。第二天星期五的早上，他付了钱。
　　＂我完全宿醉了，＂Scholze 说。
　　但他也知道他周末没有时间工作，因此周五是他完成证明的最佳时机。想到要与过去一周他在脑海中建立的一切失去联系，然后不得不在周一重新开始，这超出了他的考虑范围。
　　Scholze 说：＂我不认为我有能力在脑海中再次重建它。＂
　　于是他加足马力并完成了证明。但事后，他并不确定自己所做的是否正确。原因不仅仅是他清除了最后一道障碍的朦胧环境。证明是如此复杂 Scholze 知道他可能漏掉了一些东西。
　　＂这是一件非常复杂的事情，有许多活动部件。当你改变这些参数之一时，很难知道哪些部件移动了多少，＂Scholze 说。
　　直到 2019 年 11 月，Scholze 才抽出时间真正写下证明。一年后，他联系了伦敦帝国理工学院的数学家 Kevin Buzzard，他也是一个名为 Lean 的证明助手项目的著名布道者。Scholze 想知道是否有可能将他的证明输入到 Lean 中——把它像软件程序一样变成代码行——这样程序就可以验证它是否真的正确。
　　Buzzard 与包括弗莱堡大学博士后研究员 Johan Commelin（约翰·科梅林） 在内的少数精益社区成员分享了 Scholze 的咨询。Commelin 拥有适合这份工作的完美背景——他已经使用 Lean 多年并且熟悉＂凝聚数学＂——并且他相信验证 Scholze 的证明对于证明助手在数学界的地位合法化有很大帮助。
　　＂能够在这样一个项目上与彼得合作并附上他的名字对Lean来说将是一个巨大的推动，＂Commelin 说。
　　但他也认为这可能需要一年或更长时间才能完成，这让他犹豫了。Commelin 担心他可能会花完所有的时间来验证证明，最后，数学界的其他人只会耸耸肩。
　　＂我想，如果我花两年时间研究这个，然后走出我的洞穴说，‘这很好’，世界其他地方会说，‘哇，我们已经知道了，彼得证明了这一点， ＂＂Commelin 说。舒尔茨本人并不完全确定也没关系。
　　因此，Commelin 问 Scholze，他是否愿意发表公开声明，证明这项工作的重要性。Scholze 同意了，并于 2020 年 12 月 5 日在 Buzzard 的博客上写了一篇文章。
　　他们将其称为＂液体张量实验＂（Liquid Tensor Experiment），这是对称为液体实向量空间的证明中涉及的数学对象以及他和 Commelin 喜欢的称为液体张力实验（Liquid Tension Experiment）的前卫摇滚乐队的致敬。在 4,400 字的入门书中，Scholze 解释了结果的一些技术方面，然后添加了一个注释，用通俗的语言见证他认为用计算机检查它的重要性。
　　＂我认为这可能是我迄今为止最重要的定理。（到目前为止，它还没有真正的应用，但我相信这会改变，）＂Scholze 写道。＂最好确定它是正确的……＂
　　保证到位后，Commelin 开始工作。在向 Lean 解释了他最终希望程序检查其证明的数学陈述之后，他将更多的数学家带入了该项目。他们确定了一些引理——证明中的中间步骤——看起来最容易理解。他们首先将这些形式化，在Lean中用来确定给定陈述是否正确的数学知识库之上对它们进行编码。
　　去年 10 月，量子杂志报道过，用Lean编写数学的集体努力具有＂建造农屋的气氛＂（barn raising: 西方农村里的一种庆典,当一家人要建个新农屋时,邻居们也一起过来帮忙凑热闹,场面很喜庆）。这个项目也不例外。Commelin 将识别证明的离散部分并将它们发布到 Zulip，一个作为Lean社区中心的讨论板。当数学家看到符合他们专业知识的证明的一部分时，他们会自愿将其形式化。
　　Mehta 是为这项工作做出贡献的十几位数学家之一。5 月，他看到了 Commelin 的一篇帖子，请求帮助将一个名为 Gordan 引理的陈述的证明形式化，该陈述与 Mehta 在组合几何领域的工作有关。他花了一周时间，用与数学家正在构建的更大的证明一致的术语对证明进行编码。他说，这是Lean工作方式的象征。
　　他说：＂这是一次与很多人的大合作，他们正在做他们擅长的事情来制作一个奇异的独石柱。＂
　　随着工作的进行，Scholze 始终如一地出现在 Zulip 上，回答问题并解释证明要点——有点像建筑师在工作现场为建筑工提供指导。＂他总是触手可及，＂Commelin 说。
　　5 月底，该小组完成了 Scholze 最不确定的证明的一部分。5 月 29 日凌晨 1 点 10 分，Commelin 敲入了最后的按键。Lean 编译了证明，它像一个正常运行的程序一样运行，终于验证 Scholze 的工作是 100% 正确的。现在 Scholze 和其他数学家可以将这些技术从真正的泛函分析应用到凝聚集，因为他们知道他们肯定会在这个新环境中工作。
　　虽然 Scholze 仍然喜欢在脑海中找出证据，但 Lean 的能力给他留下了深刻的印象。他现在可以预见像它这样的程序在研究数学中发挥持久的作用。
　　＂这个实验彻底改变了我对 [证明助手] 能力的印象，＂Scholze 说。＂我现在认为原则上在Lean中将你想要的任何内容形式化是明智的。没有真正的障碍。＂