菲尔兹奖得主舒尔茨没做到的事，现在被计算机证明了

Posted 2021-09-05 QbitAl

晓查 发自 凹非寺
量子位 报道 | 公众号 QbitAI

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

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

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

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

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

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

寻求计算机验证

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

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

这是一项双赢的合作。

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

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

△ Kevin Buzzard

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