350年以上にわたり数学者を悩ませてきた「フェルマーの最終定理」。その現代的な証明を、AIがコンピュータでチェック可能なかたちに完全形式化したと発表されました。専門家が「何年もかかる」と見ていたプロジェクトが、AIアシスタントによって一気に前進し、数学の証明のあり方そのものを揺さぶる出来事となっています。
偉業の概要：フェルマーの最終定理をAIが形式化
フェルマーの最終定理とは何か
フェルマーの最終定理は、「n が 3 以上の整数のとき、x^n + y^n = z^n を満たす自然数解 (x, y, z) は存在しない」という主張です。17世紀にピエール・ド・フェルマーが余白に書き残したとされるこの一文は、その後350年以上、誰も完全な証明を示せず、「数学最大の難問」の一つとして知られてきました。
1995年のワイルズによる歴史的証明
1995年、英国の数学者アンドリュー・ワイルズ卿がついにこの定理の証明に成功しました。楕円曲線やモジュラー形式といった高度な理論を駆使したその証明は極めて複雑で、専門家による精査にも長い時間が必要でした。この「人間による歴史的証明」が、今回初めてコンピュータが検証可能な形にまで細かく書き下ろされたのが今回の成果です。
Leanを用いた世界最大規模の形式化証明
今回のプロジェクトでは、数学用の定理証明支援システム「Lean（リーン）」が用いられました。AIアシスタント「Claude（クロード）」の支援のもと、フェルマーの最終定理の証明全体が Lean で扱える形式に落とし込まれ、そのコード量はなんと1,300万行超。これは、Lean 史上最大規模の証明であり、専門家が「完成までには長年かかるだろう」と見ていた規模のプロジェクトでした。
形式化で何が変わるのか：数学の信頼性と再利用性
「正しさ」を機械がチェックできるインフラ
従来、難解な証明の正しさは、専門家コミュニティが長期間かけて読み解き、相互にチェックすることで担保されてきました。しかし、複雑さが増す現代数学では、人間だけで誤りを見逃さずに査読することがますます難しくなっています。形式化証明では、論理の一歩一歩を厳密な形で記述し、コンピュータが自動的に整合性をチェックするため、「証明が間違っていないか」という不安を大きく減らせる点が最大の利点です。
2万9,000本以上の定理も同時に形式化
今回形式化されたのは、フェルマーの最終定理そのものだけではありません。その証明の過程で必要になる関連定理や補題など、2万9,000本を超える他の定理も、さまざまな数学分野にわたって形式化されました。これらは、今後の数学研究で再利用できる「部品」として、Lean の標準ライブラリ（Mathlib）に蓄積され、次の研究や証明を効率化する土台となります。
数学知識の「インフラ整備」としての意義
研究者たちは、この取り組みを「数学知識のコアを固めていく長いプロセスの大きな一歩」と位置づけています。数世紀にわたる数学者の成果、そして Lean や Mathlib に貢献してきた多数の開発者・研究者の努力の上に、AIが新たな層を積み重ねた形です。人間とAI、ソフトウェアコミュニティが協調して「数学のインフラ」を作り上げていく象徴的な事例と言えるでしょう。
AIと数学のこれから：証明の生産性と査読負担の軽減
急増する数学論文と「査読の限界」
近年、数学を含むあらゆる分野で、研究論文の数は指数関数的に増え続けています。複雑な新理論や長大な証明も珍しくなくなり、「本当に正しいのか」を検証する査読者の負担は増す一方です。もし重大な誤りを含んだ結果がそのまま引用され続ければ、後続研究全体の信頼性にも影響しかねません。
AIアシストによる形式化で査読を支える
研究チームは、AIが支援する形式化と機械検証が、こうした課題の解決に貢献すると期待しています。AIが証明の草稿を自動的に形式化し、定理証明支援システムが論理の整合性を確認すれば、人間の査読者は「正しさの細部チェック」から「アイデアや構成の妥当性評価」へと役割をシフトできます。今回のフェルマーの最終定理の事例は、その可能性を大規模に示したものと言えます。
若手研究者・教育への波及効果
形式化された証明は、教育面でも価値があります。証明が細かなステップに分解されているため、学習者は「どこでどの定理が使われているのか」「どの前提が不可欠なのか」を機械的にたどることができます。将来的には、難解な定理の学習や、大学院レベルの高度な授業でも、AIと形式化証明が「インタラクティブな教科書」として活用される可能性があります。
まとめ
AIアシスタント Claude による、Lean を用いたフェルマーの最終定理の形式化証明は、1,300万行超のコードと2万9,000本以上の定理を含む、史上最大級のプロジェクトとなりました。これは、個々の有名定理の「正しさ確認」を超え、数学全体の信頼性と再利用性を高めるインフラづくりの一環でもあります。今後、AIと人間が協力して数学の知識基盤を整備していくことで、より速く、より確かな形で新しい発見が積み重ねられていくことが期待されます。
