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

Posted 人工智能博士

tags:

篇首语:本文由小常识网(cha138.com)小编为大家整理,主要介绍了菲尔兹奖得主舒尔茨没做到的事,现在被计算机证明了相关的知识,希望对你有一定的参考价值。

点上方人工智能算法与Python大数据获取更多干货

在右上方 ··· 设为星标 ★,第一时间获取资源

仅做学术分享,如有侵权,联系删除

转载于 :量子位

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

他和哥本哈根大学的数学家达斯汀·克劳森,多年来一直致力于一个名为“凝聚态数学”(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

---------♥---------

声明:本内容来源网络,版权属于原作者

图片来源网络,不代表本公众号立场。如有侵权,联系删除

AI博士私人微信,还有少量空位

如何画出漂亮的深度学习模型图?

如何画出漂亮的神经网络图?

一文读懂深度学习中的各种卷积

点个在看支持一下吧

以上是关于菲尔兹奖得主舒尔茨没做到的事,现在被计算机证明了的主要内容,如果未能解决你的问题,请参考以下文章

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

最年轻菲尔兹奖得主:我用计算机辅助证明研究“大一统”理论

菲尔兹奖得主再次突破数论难题:多少整数能写成2个有理数立方和?结论直接影响“千禧难题”之七...

又有3位顶级数学家加盟华为,都是菲尔兹奖得主

又有 3 位顶级数学家加盟华为,都是菲尔兹奖得主

提出量子计算机的俄罗斯数学家去世了,享年85岁,门下2位菲尔兹奖得主