陶哲軒上新項目：Lean中證明素數定理，研究藍圖都建好了

AIGC動態歡迎閱讀

原標題：陶哲軒上新項目：Lean中證明素數定理，研究藍圖都建好了
關鍵字：定理,素數,數學家,數論,項目
文章來源：機器之心
內容字數：2731字

內容摘要：

機器之心報道
編輯：陳萍借助 Lean，陶哲軒又開始了新的項目。「由 Alex Kontorovich 和我領導的一個新的 Lean 形式化項目剛剛正式宣布，該項目旨在形式化素數定理（prime number theorem，PNT）的證明，以及伴隨而來的復分析和解析數論的支持機制，并計劃給出進一步的結果如 Chebotarev 密度定理。」著名數學家陶哲軒在個人博客中寫道。素數定理是數學中的一個重要定理，描述了素數在自然數中的分布規律，該定理在數論中是一個比較重要的研究方向。
形式化證明本質上是一種計算機程序，但與 C++ 或 Python 中的傳統程序不同，證明的正確性可以用證明助手（比如 Lean 語言）來驗證。舉例來說，陶哲軒在論文《A MACLAURIN TYPE INEOUALITY》中給出的證明只有不到一頁，但形式化證明使用了 200 行 Lean 語言。而陶哲軒的合作者 Alex Kontorovich 也是一位非常著名的數學家，現為羅格斯大學數學系特聘教授，主要研究方向是數論。目前，這兩位數學家合作的 Lean 形式化項目「PrimeNumberTheoremAnd」

原文鏈接：陶哲軒上新項目：Lean中證明素數定理，研究藍圖都建好了

聯系作者

文章來源：機器之心
作者微信：almosthuman2014
作者簡介：專業的人工智能媒體和產業服務平臺