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

百家 作者:量子位 2021-08-12 14:01:54 阅读:248
晓查 发自 凹非寺
量子位 报道 | 公众号 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

本文系网易新闻•网易号特色内容激励计划签约账号【量子位】原创内容,未经账号授权,禁止随意转载。

「智能汽车」交流群招募中!

欢迎关注智能汽车、自动驾驶的小伙伴们加入社群,与行业大咖交流、切磋,不错过智能汽车行业发展&技术进展。加好友请务必备注您的姓名-公司-职位哦~



点这里

关注公众号:拾黑(shiheibook)了解更多

[广告]赞助链接:

四季很好,只要有你,文娱排行榜:http://www.yaopaiming.com/
让资讯触达的更精准有趣:https://www.0xu.cn/

图库