AIがフェルマーの最終定理の形式化を11日で達成 1300万行で完全検証

AIが数学すうがくの歴史的れきしてきな難問なんもんである「フェルマーの最終定理さいしゅうていり」の形式化けいしきかを11日間にちかんで完成かんせいさせました。Anthropicの研究者けんきゅうしゃであるティエンイー・ペン氏しらの発表はっぴょうによると、AIモデルのClaudeが約やく1300万行まんぎょうに及およぶコードを生成せいせいし、コンピューターで完全かんぜんに検証けんしょうできる証明しょうめいを構築こうちくしました。形式化けいしきかとは、人間にんげん向むけの数学的すうがくてきな論理ろんりを、証明支援しょうめいしえんシステム「Lean」のようなコンピューターが厳密げんみつにチェックできる形かたちへ書かき直なおす作業さぎょうのことです。

フェルマーの最終定理さいしゅうていりは、17世紀せいきにピエール・ド・フェルマー氏しが提唱ていしょうして以来いらい350年ねん以上いじょうにわたって未解決みかいけつでしたが、1995年ねんにアンドリュー・ワイルズ氏しらが129ページに及およぶ論文ろんぶんで証明しょうめいを完成かんせいさせました。解明かいめいされたものの、人間にんげんによる論文ろんぶんの検証けんしょうには数すうカ月げつを要ようしました。さらに、人間にんげん向むけの論文ろんぶんでは「明あきらか」として省略しょうりゃくされがちな細こまかな論理ろんりも、コンピューターに確認かくにんさせるにはすべての手順てじゅんを厳密げんみつに記述きじゅつしなければなりません。インペリアル・カレッジ・ロンドンのケビン・バザード氏しらの研究けんきゅうチームが2024年ねんから進すすめている共同きょうどうプロジェクトでも、形式化けいしきかには数年すうねんかかると見込みこまれていました。

Anthropicが数十すうじゅうのClaudeエージェントを投入とうにゅうした初期しょきの試こころみでは、各かくエージェントがプロジェクト全体ぜんたいの進捗しんちょくを把握はあくできず、互たがいの成果せいかを再利用さいりようできないといった課題かだいが生しょうじました。そこでペン氏しらは、数学すうがく形式化けいしきか用ようの共同作業きょうどうさぎょうプラットフォーム「Prove2Me」を開発かいはつしました。Prove2Meは定理ていり同士どうしの依存関係いぞんかんけいを有向非巡回ゆうこうひじゅんかいグラフ（DAG）で管理かんりし、各かくAIが次つぎに証明しょうめいすべき命題めいだいを明確めいかくに把握はあくできるようにしました。さらに、定理ていりの記述きじゅつと証明しょうめいを別べつファイルに分離ぶんりしてコンパイルを高速化こうそくかし、自然言語しぜんげんごによる説明せつめいを付与ふよすることで検索性けんさくせいを高たかめました。その結果けっか、Claudeは11日間にちかんで約やく3万まん300件けんの定理ていりを証明しょうめいし、そのうち約やく2万まん9500件けんを最終的さいしゅうてきな証明しょうめいに組くみ込こむことに成功せいこうしました。

完成かんせいしたコードの規模きぼは約やく1300万行まんぎょうに上のぼり、標準的ひょうじゅんてきな数学すうがくライブラリ「Mathlib」の5倍ばい以上いじょうに達たっします。この証明しょうめいは未証明みしょうめい部分ぶぶんを残のこす「sorry」などの一時的いちじてきな記述きじゅつを含ふくまず、Leanの標準的ひょうじゅんてきな3つの公理こうりのみに依存いぞんしています。さらに、Rust言語げんごで書かかれた独立どくりつした検証けんしょうプログラム「nanoda」による検査けんさでも、100万件まんけん以上いじょうの宣言せんげんがエラーなしで検査けんさされました。AIが大量たいりょうの複雑ふくざつな証明しょうめいを高速こうそくに生成せいせいできるようになるにつれ、人間にんげんだけで検証けんしょうする負担ふたんは増大ぞうだいしています。Anthropicは将来しょうらい、人間にんげんの読者どくしゃ向むけの論文ろんぶんと並行へいこうして、コンピューターで自動検証じどうけんしょうできる形式化けいしきかされた証明しょうめいを併記へいきして公開こうかいすることが数学界すうがくかいの標準ひょうじゅんになると予測よそくしています。