「由 Alex Kontorovich 和我領(lǐng)導(dǎo)的一個(gè)新的 Lean 形式化項(xiàng)目剛剛正式宣布，該項(xiàng)目旨在形式化素?cái)?shù)定理（prime number theorem，PNT）的證明，以及伴隨而來的復(fù)分析和解析數(shù)論的支持機(jī)制，并計(jì)劃給出進(jìn)一步的結(jié)果如 Chebotarev 密度定理。」著名數(shù)學(xué)家陶哲軒在個(gè)人博客中寫道。

素?cái)?shù)定理是數(shù)學(xué)中的一個(gè)重要定理，描述了素?cái)?shù)在自然數(shù)中的分布規(guī)律，該定理在數(shù)論中是一個(gè)比較重要的研究方向。

形式化證明本質(zhì)上是一種計(jì)算機(jī)程序，但與 C++ 或 Python 中的傳統(tǒng)程序不同，證明的正確性可以用證明助手（比如 Lean 語言）來驗(yàn)證。舉例來說，陶哲軒在論文《A MACLAURIN TYPE INEOUALITY》中給出的證明只有不到一頁，但形式化證明使用了 200 行 Lean 語言。

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

目前，這兩位數(shù)學(xué)家合作的 Lean 形式化項(xiàng)目「PrimeNumberTheoremAnd」已經(jīng)上傳到 GitHub 上。

項(xiàng)目地址：https://github.com/AlexKontorovich/PrimeNumberTheoremAnd

因?yàn)樵擁?xiàng)目剛建立不久，陶哲軒以及 Alex Kontorovich 還為此構(gòu)建了一幅藍(lán)圖：

藍(lán)圖地址：https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/

可以看出該藍(lán)圖包含 5 個(gè)部分：

第一部分介紹了項(xiàng)目的首要目標(biāo)是在 Lean 中證明素?cái)?shù)定理。他們表示該問題仍然是 Wiedijk 列出的需要形式化的 100 個(gè)定理中突出的問題之一。值得注意的是，PNT 之前已被形式化過，由 Avigad 等人在 Isabelle 中完成。而該項(xiàng)目的目標(biāo)是將這項(xiàng)工作擴(kuò)展到級數(shù)中的素?cái)?shù)（Dirichlet 定理）、Chebotarev 密度定理等等。

目前，完成上述目標(biāo)可以考慮下面三種方法：

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

第二種是開發(fā)一些復(fù)分析，包括在矩形上的殘差計(jì)算（residue calculus on rectangles）、參數(shù)原理（argument principle）和 Mellin 變換，從而得出一個(gè)僅包含漸近公式的素?cái)?shù)定理（PNT）的證明（對應(yīng)第三部分）。

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

最后一部分是基本推論。

其實(shí)回顧陶哲軒以往的研究，他都多次都提到過 Lean。簡單來講，Lean 是一種可幫助數(shù)學(xué)家驗(yàn)證定理的編程語言，用戶可以在其中編寫和驗(yàn)證證明。相比初代 Lean，現(xiàn)在最新的 Lean 4 版本進(jìn)行了多項(xiàng)優(yōu)化，包括更快的編譯器、改進(jìn)的錯(cuò)誤處理和更好的與外部工具集成的能力等。現(xiàn)在，陶哲軒他們又將該工具用于素?cái)?shù)定理的形式化證明，可見 Lean 已成為數(shù)學(xué)研究中的得力助手。