テレンス・タオが新プロジェクトを立ち上げ：リーンで素数定理を証明、研究計画は完成

「アレックス・コントロヴィッチと私が率いる新しいリーン形式化プロジェクトが正式に発表されました。このプロジェクトは、素数定理（PNT）の証明と、複素解析および解析的数論の付随するサポートメカニズムを形式化することを目的としており、チェボタレフの密度定理などのさらなる結果を出す予定です」と有名な​​数学者テレンス・タオは個人ブログに書いています。

素数定理は数学における重要な定理であり、自然数における素数の分布法則を記述します。この定理は、数論における比較的重要な研究方向です。

正式な証明は本質的にはコンピュータ プログラムですが、C++ や Python の従来のプログラムとは異なり、証明の正確性は証明支援ツール (Lean 言語など) を使用して検証できます。たとえば、Terence Tao が論文「A MACLAURIN TYPE INEOUALITY」で示した証明は 1 ページ未満ですが、正式な証明には 200 行の Lean 言語が使用されています。

タオの共同研究者であるアレックス・コントロヴィッチも非常に有名な数学者です。彼は現在、ラトガース大学数学科の著名な教授です。彼の主な研究分野は数論です。

現在、二人の数学者が共同で開発したLean形式化プロジェクト「PrimeNumberTheoremAnd」がGitHubにアップロードされています。

プロジェクトアドレス: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd

このプロジェクトは設立されたばかりだったため、Terence Tao 氏と Alex Kontorovich 氏はその青写真も作成しました。

ブループリントのアドレス: https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/

青写真には 5 つの部分が含まれていることがわかります。

最初の部分では、Lean で素数定理を証明するというプロジェクトの主な目標を紹介します。この問題は、定式化が必要なヴィーディクの100の定理のリストの中で未解決の問題の1つとして残っていると彼らは言う。 PNT は、Avigad らによる Isabelle で以前に形式化されていたことは注目に値します。このプロジェクトの目標は、この研究を素数級数（ディリクレの定理）、チェボタレフの密度定理などに拡張することです。

現在、上記の目標を達成するために、次の 3 つの方法が考えられます。

最も速いのは、Michael Stoll が提案した「オイラー積」プロジェクトです。このプロジェクトでは、PNT の証明において、ウィーナー-池原タウバー定理 (第 2 部に相当) のみが欠けています。

2 つ目は、長方形上の留数計算、引数原理、メリン変換などの複雑な解析を展開し、漸近式のみを含む素数定理 (PNT) の証明 (パート III に対応) を導きます。

3 番目の方法は、3 つの方法の中で最も一般的であり、アダマール因数分解定理、ホフシュタイン-ロックハート過程などが含まれます (4 番目の部分に相当)。

最後の部分は基本的な推論です。

実際、テレンス・タオの以前の研究を振り返ると、彼は何度もリーンについて言及しています。簡単に言えば、Lean は数学者が定理を検証するのに役立つプログラミング言語であり、ユーザーは証明を記述して検証することができます。 Lean の第 1 世代と比較して、最新の Lean 4 バージョンでは、コンパイラの高速化、エラー処理の改善、外部ツールとの統合の改善など、多くの最適化が行われています。現在、テレンス・タオ氏とその同僚はこのツールを使って素数定理を正式に証明しており、リーンが数学研究の強力な助手となっていることが示されています。