因数学家“液体张量实验”留名，微软计算机验证打破偏见

德国著名数学家、菲尔兹奖得主皮特・舒尔茨遇到了一个难题。

他和哥本哈根大学的数学家达斯汀・克劳森，多年来一直致力于一个名为“凝聚态数学”（Condensed Mathematics）的问题。

他俩发现，因为拓扑学的传统概念，导致三个数学领域（几何、泛函分析和 p 进数）之间不兼容，如果创建一种新的基础概念，就可以实现一个“大统一”理论。

但是，在研究这个问题过程中，舒尔茨遇到了一个特别重要且困难的证明。

2019 年 7 月的一周，舒尔茨开始在脑海中开始自己的证明，几乎没有借助纸笔。直到 11 月，舒尔茨才完整写下了证明。

但是证明过程是如此复杂，连舒尔茨都不敢保证证明中是否有纰漏。

寻求计算机验证

一年后，舒尔茨联系了伦敦帝国理工学院的数学家 Kevin Buzzard，他是“Lean”的布道者。

Lean 是微软研究院在 2013 年推出的计算机定理证明器：数学家可以把数学公式转换成代码，再输入到 Lean 中，让程序来验证定理是否正确。

这是一项双赢的合作。

舒尔茨把他的证明输入到 Lean 中，可以验证自己是否正确。

对于 Buzzard 来说，这是为 Lean 扬名的大好机会，如果能和舒尔茨这样的天才数学家联名，无疑对计算机辅助证明在数学界的合法化有很大帮助。

Buzzard 向 Lean 社区的其他成员分享了舒尔茨的证明，其中就包括弗莱堡大学的博士后 Johan Commelin。

“能够在这样一个项目上与彼得合作并附上他的名字，对 Lean 来说是一个巨大的宣传。”Commelin 说。

但是，如果证明花的时间太长，数学界的人不会意识到这项工作的重要性，他们会说：“哦，我们已经知道舒尔茨证明了这一点。”

因此，Commelin 问舒尔茨，是否愿意发表公开声明，证明这项工作的重要性。舒尔茨答应了。

舒尔茨公布实验结果

2020 年 12 月 5 日，舒尔茨在 Buzzard 的博客上公布了证明结果，在这篇 4000 多字的文章中，舒尔茨用通俗的语言证明计算机验证的重要性。

他们把这项验证实验叫做“液体张量实验”，这既是对液体实向量空间的证明中涉及的数学对象的一种致敬，也是对两位数学家喜欢的摇滚乐队“液体张力实验”的致敬。

舒尔茨说这个定理可能是他“迄今为止最重要的定理”。

Commelin 将舒尔茨的问题发布到一个名叫 Zulip 社区上，由十几位数学家协力完成，每个人都在自己擅长的领域构建证明代码。

随着工作的进行，舒尔茨始终如一地出现在 Zulip 社区上，回答问题并解释证明要点，有点像建筑师在工作现场为提供指导一样。

5 月 29 日凌晨 1 点 10 分，Commelin 输入了最后的回车键。Lean 编译了整个证明，验证舒尔茨的工作是 100% 正确的。

虽然舒尔茨仍然喜欢在脑海中寻找证明，但 Lean 的能力给他留下了深刻的印象。

“这个实验彻底改变了我对（计算机辅助证明）能力的印象，”舒尔茨说。

日渐成熟的 Lean

帮助舒尔茨只是 Lean 这么多年中的一项工作而已，这个最初由微软研究院开源的数学证明器，如今已经得到许多数学家的支持。

聚集在 Zulip 上的数学家正在为 Lean 构建一个数学知识库 mathlib。截至今日，mathlib 已经包含了 26492 条定义和 58738 条定理。

Buzzard 多年来一直在进行一项计划，就是将帝国理工学院的整个本科数学课程用 Lean 写成代码，目前只完成了一半。

但是正在为 Lean 完善数学库的人几乎可以肯定，在几年内，Lean 至少能够理解本科高年级期末考试中的问题。

如今 Lean 已经进化到第四代，今年微软还让它参加了 IMO。不过，Lean 到底在刚刚结束的 IMO 中有怎样的发挥，官方并未公布。

参考链接：

[1]https://www.quantamagazine.org/lean-computer-program-confirms-peter-scholze-proof-20210728/

[2]https://www.quantamagazine.org/building-the-mathematical-library-of-the-future-20201001/

[3]https://github.com/leanprover/lean4

广告声明：文内含有的对外跳转链接（包括不限于超链接、二维码、口令等形式），用于传递更多信息，节省甄选时间，结果仅供参考，IT之家所有文章均包含本声明。