陶哲軒上新專題：Lean中證明質數定理，研究藍圖都建好了

借助 Lean，陶哲軒又開始了新的專案。

「由Alex Kontorovich 和我領導的一個新的Lean 形式化專案剛剛正式宣布，該專案旨在形式化素數定理（prime number theorem，PNT）的證明，以及伴隨而來的複分析和解析數論的支持機制，併計劃給出進一步的結果如Chebotarev 密度定理。」著名數學家陶哲軒在個人博客中寫道。

素數定理是數學中的一個重要定理，描述了質數在自然數中的分佈規律，該定理在數論中是一個比較重要的研究方向。

形式化證明本質上是一種電腦程序，但與C 或Python 中的傳統程式不同，證明的正確性可以用證明助手（例如Lean 語言）來驗證。舉例來說，陶哲軒在論文《A MACLAURIN TYPE INEOUALITY》中給出的證明只有不到一頁，但形式化證明使用了 200 行 Lean 語言。

而陶哲軒的合作者 Alex Kontorovich 也是一位非常著名的數學家，現為羅格斯大學數學系特聘教授，主要研究方向是數論。

目前，這兩位數學家合作的 Lean 形式化專案「PrimeNumberTheoremAnd」已經上傳到 GitHub 上。

專案網址：https://github.com/AlexKontorovich/PrimeNumberTheoremAnd

因為專案剛建立不久，陶哲軒以及Alex Kontorovich 也為此建構了一幅藍圖：

藍圖位址：https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/

可以看出該藍圖包含5 個部分：

#第一部分介紹了專案的首要目標是在Lean 中證明素數定理。他們表示該問題仍然是 Wiedijk 列出的需要形式化的 100 個定理中突出的問題之一。值得注意的是，PNT 先前已被形式化過，由 Avigad 等人在 Isabelle 中完成。而這個專案的目標是將這項工作擴展到級數中的質數（Dirichlet 定理）、Chebotarev 密度定理等等。

目前，完成上述目標可以考慮以下三種方法：

#最快的是Michael Stoll 提出的「歐拉積」項目，該項目對PNT 的證明只缺少Wiener-Ikehara Tauberian 定理（對應第二部分）。

第二種是發展一些複分析，包括  residue calculus on rectangles 、 argument principle 和Mellin 變換，從而得出一個僅包含漸近公式的質數定理（PNT ）的證明（對應第三部分）。

第三種方法，也是三種方法中最通用的一種，包括阿達馬因子分解定理、Hoffstein-Lockhart 等過程（對應第四部分）。

最後一部分是基本推論。

其實是回顧陶哲軒以往的研究，他都多次提到 Lean。簡單來講，Lean 是一種可幫助數學家驗證定理的程式語言，使用者可以在其中編寫和驗證證明。相較於初代 Lean，現在最新的 Lean 4 版本進行了多項最佳化，包括更快的編譯器、改進的錯誤處理和更好的與外部工具整合的能力等。現在，陶哲軒他們又將該工具用於質數定理的形式化證明，可見 Lean 已成為數學研究中的得力助手。

以上是陶哲軒上新專題：Lean中證明質數定理，研究藍圖都建好了的詳細內容。更多資訊請關注PHP中文網其他相關文章！