菲爾茲獎得主舒爾茨沒做到的事,現在被計算機證明了

人工智能博士 2021-08-15 07:23:38 阅读数:379

本文一共[544]字,预计阅读时长:1分钟~
得主 做到 在被 明了

點上方人工智能算法與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博士私人微信,還有少量空比特

如何畫出漂亮的深度學習模型圖?

如何畫出漂亮的神經網絡圖?

一文讀懂深度學習中的各種卷積

點個在看支持一下吧

版权声明:本文为[人工智能博士]所创,转载请带上原文链接,感谢。 https://gsmany.com/2021/08/20210815072333744Q.html