Lean の助けを借りて、Tao Zhexuan は新しいプロジェクトを開始しました。
「Alex Kontorovich と私が率いる新しいリーン形式化プロジェクトが正式に発表されました。これは、素数定理 (素数) を形式化することを目的としています。有名な数学者テレンス・タオ氏は、自身のブログにこう書いている。 
素数定理は自然数における素数の分布を記述する数学の重要な定理であり、整数論における重要な研究方向です。 形式的証明は本質的にはコンピューター プログラムですが、C や Python による従来のプログラムとは異なり、証明の正しさは証明アシスタント (リーン言語など) を使用して検証できます。検証します。たとえば、テレンス・タオが論文「A MACLAURIN TYPE INEOUALITY」で示した証明は 1 ページ未満ですが、正式な証明では 200 行の無駄のない言語が使用されています。 
Tao Zhexuan 氏の共同研究者である Alex Kontorovich 氏も非常に有名な数学者で、現在はラトガース大学数学部の高名な教授を務めており、彼の主な研究方向は数論です。 
現在、この二人の数学者が共同開発したリーン公式プロジェクト「PrimeNumberTheoremAnd」がGitHubにアップロードされています。 
プロジェクト アドレス: https://github.com/AlexKontorovich/PrimeNumberTheoremAndプロジェクトはまだ作成されたばかりなので、 Terence Tao と Alex Kontorovich もこのためのブループリントを構築しました: 
ブループリントのアドレス: https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/ ブループリントには 5 つの部分が含まれていることがわかります。 最初の部分では、プロジェクトの主な目標を紹介します。リーン定理で素数を証明します。彼らは、この問題は依然として形式化が必要な 100 の定理の Wiedijk のリストの中で未解決の問題の 1 つであると述べています。 PNT は、Avigad らによって Isabelle で以前に形式化されていることに注目する価値があります。そして、このプロジェクトの目標は、この研究を級数の素数 (ディリクレの定理) やチェボタレフの密度定理などに拡張することです。 上記の目標を達成するには、現在、次の 3 つの方法が考えられます。 最も速い方法は、によって提案されています。 Michael Stoll の「オイラー積」プロジェクト、このプロジェクトの PNT の証明には、ウィナー - 池原のタウベリアン定理 (第 2 部に相当) が欠けているだけです。 2 つ目は、漸近公式のみを含む素数定理 (PNT) につながる、長方形の留数計算、引数原理、メリン変換などの複雑な解析を開発することです。) （第3部に相当）。 3 番目の方法は、アダマール因子分解定理、ホフシュタイン ロックハート法、およびその他のプロセス (4 番目の部分に相当) を含む 3 つの方法の中で最も一般的な方法でもあります。 #最後の部分は基本的な推論です。
実際、Tao Zhexuan のこれまでの研究を振り返ると、彼は Lean について何度も言及しています。簡単に言うと、リーンは数学者が定理を検証するのに役立つプログラミング言語であり、ユーザーは証明を書いて検証することができます。オリジナルの Lean と比較して、最新の Lean 4 バージョンでは、コンパイラの高速化、エラー処理の改善、外部ツールとの統合の改善など、多くの最適化が行われています。現在、テレンス・タオらは素数定理の正式な証明にこのツールを使用しており、リーンが数学研究の強力なアシスタントとなっていることがわかります。
以上がTao Zhexuan の新しいプロジェクト: Lean で素数定理を証明し、研究の青写真が完成しましたの詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。
