300 年以上にわたるリレー: テレンス・テルに触発されて、数学者たちは AI を使用してフェルマーの最終定理の証明を形式化することに決めました。

テレンス・タオに触発されて、数学的探求に人工知能を使用しようとする数学者が増えています。今回のターゲットは、世界トップ10に入る数学の難問「フェルマーの最終定理」。フェルマーの最終定理は非常に複雑な数学的問題であり、これまでのところ実現可能な解決策は見つかっていません。数学者は、人工知能の強力な計算能力とインテリジェントなアルゴリズムの助けを借りて、数学で探究できることを望んでいます

フェルマーの最終定理は、「フェルマーの最終定理」とも呼ばれます。 (FLT)」は、17 世紀のフランスの数学者ピエール・ド・フェルマーによって提唱されました。その背景には伝説的な物語があります。 1637 年頃、フェルマーがディオファントスの『算術』のラテン語訳を読んでいたとき、第 11 巻の命題 8 の隣に次のように書いたと言われています。 「私はこれについて何かを発見したと確信しています。これは素晴らしいデモンストレーションですが、残念ながら、ここの空白スペースは小さすぎて書き込むことができません。

#この段落の前に記載されているのは、フェルマーの最終定理の内容です。整数 n > 2 のとき、x^n y^n=z^n についての方程式が成り立ちます。

フェルマーはそれを証明する方法を知っていると述べましたが、本の空白部分が小さすぎるため、物語の信憑性やフェルマーが本当に理解したかどうかについては書きませんでした。この証明方法は後世で議論の的となっており、数学者たちは 1995 年まで 8 年間を費やしてフェルマーの最終定理を証明してきました。

フェルマーの最終定理が証明されたので、数学者は AI で他に何ができるでしょうか? 答えは、その証明を形式化することです。

##数学における形式化とは、通常、厳密な形式言語 (論理や集合論など) を使用して数学的オブジェクト、構造、定理、証明を表現し、コンピューター上で表現、検証、操作できるようにすることを指します。数学的内容の正確性と一貫性を確保すること。形式数学の発展は 19 世紀後半から 20 世紀初頭まで遡ることができますが、現代形式数学は 20 世紀に始まった数理論理学とコンピュータ サイエンスの発展です。 形式数学の主な目標は、一連の記号、一連の基本公理、および一連の推論規則を含む形式システムを、これらの規則と公理の適用を通じて確立することです。昨年の Tao Zhexuan らは、ある論文を形式化するために Lean (対話型定理証明器およびプログラミング言語) を使用したことがありました。この論文は、多項式フライマン-ルザ予想のバージョンの証明であり、昨年 11 月に arXiv に投稿されました。リーン言語コードを作成する際、Tao Zhexuan 氏は AI プログラミング アシスタントの Copilot も使用しました。この事件は数学と人工知能のコミュニティで広く注目を集めました。

当時、リーンテクノロジーオープンソースコミュニティの最も重要な推進者であるインペリアル・カレッジ・ロンドンのケビン・バザード氏は、「基本的に、何かをデジタル化すると、それを新しい方法で使用できることは明らかです」と述べました。 「私たちは数学をデジタル化します。それによって数学はより良くなります。」

これは、最近フェルマーの最終定理の証明を形式化すると主張した数学者のバザード教授です。ツールも無駄のないものです。

その背景や動機、具体的な方法をブログで紹介しました。

なぜフェルマーの最終定理の証明を形式化する必要があるのでしょうか?

フェルマーの最終定理の形式は非常にシンプルで直感的ですが、それを証明することは非常に困難です。これは間違いなく、数学の奥深い美しさを示す優れた例です。過去数世紀にわたって、この問題を解決するために、数学者は暗号から物理学に至るまでの分野に応用できる多数の数学理論を開発し、革新してきました。

アンドリュー ワイルズは FLT からインスピレーションを受けたかもしれませんが、実際、彼の研究はラングランズ プロジェクト、つまり数論、代数幾何学、近似を結びつけた数学における一連の広範囲にわたるアイデアに画期的な進歩をもたらしました。グループ代表者の割合は2024年になっても注目を集めています。

歴史的に、代数的整数論における他のいくつかの大きな進歩 (数体の因数分解や巡回体の算術など) は、少なくとも部分的には FLT をより深く理解したいという欲求によって動機付けられました。

ワイルズの研究は、彼の生徒であるリチャード・テイラーによって補完され、20世紀の数学の広大な基礎の上に構築されました。ワイルズによって導入された基本的な手法である「モジュール性リフティング定理」は、元の論文が出版されてから 30 年間で概念的に大幅に簡略化され、広く一般化されました。この分野は現在でも非常に活発です。 2022 年の国際数学者会議でのフランク・カレガリの論文。ワイルズの躍進以来の進歩を概説しています (参照: https://arxiv.org/abs/2109.14145)。 Kevin Buzzard 氏は、この分野での継続的な活動が FLT 証明を形式化する動機の 1 つであると述べました。

数学の形式化とは、紙上の数学を、定理や証明の概念を理解できるようにするコンピューター プログラミング言語に変換する技術です。インタラクティブ定理証明器 (ITP) としても知られるこれらのプログラミング言語は、何十年も前から存在しています。しかし、近年、この分野は数学界からある程度の注目を集めているようです。私たちは数学における研究の形式化の例をいくつか目撃してきましたが、その最新のものは、テレンス・タオらによる多項式フライマン・ルザ予想​​の証明の形式化です。この 2023 年の画期的な論文は、わずか 3 週間で Lean で正式に作成されました。このような成功物語は、リーンのような ITP が今やすべての現代数学を形式化する準備ができていると傍観者に思わせるかもしれません。

しかし、真実は決して単純ではありません。組み合わせ論などの数学の一部の分野では、現代の画期的な進歩がリアルタイムで形式化されているのが見られます。しかし、バザード氏は定期的にロンドンの整数論セミナーに参加しており、現代の数学的定義に関するリーンの知識がセミナーで発表された結果を定式化するのに不十分であり、ましてやその証明を検証するのに不十分であることによく気づいたと述べた。

実際、この側面における数論の「遅れ」は、バザードが FLT の現代的な証明の形式化を開始する主な動機の 1 つでした。プロジェクトの終わりまでに、リーンは保型形式 (複素変数の関数の特別なクラス) と表現、ガロア表現、潜在自己同型、モジュール性推進定理、代数多様体の算術、クラス体理論、算術双対定理を理解できるようになります。 、志村多様体および現代の代数整数論で使用されるその他の概念。バザード氏の見解では、これらの基盤が整備されていれば、彼自身の専門分野で起こっていることを形式化することはもはやSFではなくなるでしょう。

それでは、なぜこれを行うのでしょうか?バザード氏は、「一部のコンピューター科学者が信じているのであれば、人工知能の急激な成長により、最終的にはコンピューターが数学者の研究を支援できるようになるだろう。そのような研究は、コンピューターが現代の数学研究で何をしているのかを理解するのに役立つだろう。」と説明した。

プロジェクトをどのように実行するか?

フェルマーの最終定理の定式化プロジェクトが始動しました。 Buzzard は現在の進行状況をグラフィックで表示します。

興味のある研究者は詳細を読むことができます: https:// Imperialcollegelondon.github.io/FLT/blueprint/dep_graph_document.html

このプロジェクトは EPSRC によって後援されています。資金提供により、Buzzard は最初の 5 年間の資金を受け取ります。この期間における彼の最初の目標は、FLT を 1980 年代後半に数学者に知られていたステートメントに還元することでした。

もちろん、バザードは単独でこれを行うつもりはありませんでした。同氏は、議論の一部については基本原則は理解したが、詳細を詳しく検討したことはなかったと述べた。さらに、Project Langlands では、GL_2 の循環基底変換や Jacquet-Langlands など、いくつかの重要なことも導入されました。これらの奥深い事柄に対する彼の理解は十分に深くありません。

ただし、これこそが正式なプロジェクトの利点です。 Buzzard は、Lean で必要な結果を明確に表現し、他の人に伝えることができるようになります。このシステムの利点は、貢献するために FLT の証明全体を理解する必要がないことです。上の図は証明を多くの小さな補題に分割しているため、クラウドソーシングに非常に便利です。これらの補題のいずれかを正式に証明できれば、Buzzard はあなたのプル リクエストを心待ちにしています。

プロジェクトに参加したい人は、Lean について知っておく必要があります。このため、バザードはオンライン教科書 Mathematics in Lean を推奨しています。

教科書リンク: https://leanprover-community.github.io/mathematics_in_lean/

このプロジェクトは、Lean の FLT ストリームで実行されます。 Zulip チャットは、数学者とコンピューター科学者がリアルタイムで共同作業できる強力な研究フォーラムで、コードと数学を簡単に公開し、スレッドとストリーム システムを使用して複数の独立した会話を同時に効果的にサポートします。

Lean Zulip チャット リンク: https://leanprover.zulipchat.com/

Buzzard 氏は、プロジェクトにどれくらいの時間がかかるかわからないと述べました。しかし彼は間違いなく楽観的だ。

同時に、Lean のような正式な証明ツールも常に反復されています。オリジナルの Lean と比較して、最新の Lean 4 バージョンでは、コンパイラの高速化、エラー処理の改善、外部ツールとの統合の改善など、多くの最適化が行われています。

昨年末、オープン プラットフォームの LeanDojo チームとカリフォルニア工科大学の研究者は、大規模な言語モデルが人間と対話できるように設計されたコラボレーション ツールである Lean Copilot を立ち上げ、数学的手法に AI を導入しました。大きなモデルの力。

「適切に使用すれば、AI は 2026 年までに数学研究や他の多くの分野で信頼できる共著者になると私は予測しています。」と Tao Zhexuan 氏は以前のブログで述べました。

テレンス・タオの予言が近いうちに当たることを願っています。

関連記事:

• AI を使用したテレンス タオの正式な証明とは何ですか? PFR 予想の過去と現在を理解するための 1 つの記事>>

• Tao Zhexuan のお気に入りの証明アシスタント Lean は大規模なモデルを使用しています>>

• 大きなモデルは、テレンス タオが問題を解決し、数学の定理を証明するのに役立ちます。本当に数学は、AI の助けを借りてブレークスルーを達成する最初の科目になるのでしょうか? 》

• ##《

  Tao Zhexuan の新しいプロジェクト: Lean での素数定理の証明、研究青写真が完成しました 》

参考リンク: https://leanprover.zulipchat.com/#narrow/stream/416277-FLT

https : //mp.weixin.qq.com/s/d9RSkRhlKH5ZMek3yTqe4Q

以上が300 年以上にわたるリレー: テレンス・テルに触発されて、数学者たちは AI を使用してフェルマーの最終定理の証明を形式化することに決めました。の詳細内容です。詳細については、PHP 中国語 Web サイトの他の関連記事を参照してください。