数学家可以将数学公式转换成代码输入到Lean中让程序验证定理是否正确

德国著名数学家，菲尔兹奖获得者彼得舒尔茨遇到了一个难题

他和哥本哈根大学的数学家达斯汀克劳森多年来一直在研究一个名为浓缩数学的问题

他们发现，由于传统的拓扑概念，这三个数学领域是不相容的如果创造一个新的基本概念，就可以实现大统一理论

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

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

但证明过程如此复杂，连舒尔茨都无法保证证明中是否有瑕疵。

寻求计算机验证

一年后，舒尔茨联系了凯文布扎德，他是伦敦帝国理工学院的数学家，也是精益思想的传播者。

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

这是一个双赢的合作。

舒尔茨可以通过将他的证明输入Lean来验证他的正确性。

对于Buzzard来说，这是Lean扬名立万的绝佳机会如果他能加入像舒尔茨这样的天才数学家，无疑将有助于计算机辅助数学认证的合法化

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

能够在这样一个项目上与彼得合作，并附上他的名字，对Lean来说是一个很大的宣传鸭跖草说

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

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

舒尔茨宣布了实验结果

日前，舒尔茨在Buzzard的博客上公布了证明结果在这篇4000字的文章中，舒尔茨用通俗易懂的语言证明了计算机验证的重要性

他们把这个验证实验称为液体张量实验，这不仅是对液体实向量空间证明所涉及的数学对象的致敬，也是对两位数学家喜欢的摇滚乐队液体张力实验的致敬。

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

Commelin向一个名为Zulip的社区发布了舒尔茨的问题，这个社区由十几个数学家完成，他们每个人都在自己的领域构建了证明代码。

伴随着工作的进行，舒尔茨一直出现在Zulip社区，回答问题并解释证明的关键点，这有点像建筑师在工作现场提供指导。

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

虽然舒尔茨还是喜欢在脑子里找证据，但Lean的能力给他留下了深刻的印象。

舒尔茨说:这个实验彻底改变了我对能力的印象。

成熟的瘦肉

帮助舒尔茨只是精益这么多年的工作之一这个数学证明器最初由微软研究院开放，得到了很多数学家的支持

聚集在祖利普的数学家们正在为Lean建立一个数学知识库mathlib到目前为止，mathlib已经包含了26492个定义和58738个定理

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

可是，那些正在完善精益数学库的人几乎可以肯定，精益至少会在几年后理解高年级本科生期末考试中的问题。

现在Lean已经进化到第四代了，今年微软也让它参加了IMO可是，这位官员还没有宣布精益在刚刚结束的国际海事组织中到底是如何发挥作用的

参考链接: