AI・機械学習

フェルマーの最終定理の形式化

742 pointsby jlebar2026年9月5日479 コメント

要約

Anthropicは、AIモデルClaudeが、Leanプログラミング言語を用いてフェルマーの最終定理のコンピュータチェック済み証明を11日間で生成したと発表しました。この成果は、AIが複雑な数学的証明を自動で形式化し検証する能力を示すもので、数学研究の検証プロセスを加速する可能性を秘めています。

2026年9月4日

フェルマーの最終定理（FLT）は、3以上の自然数nについて、xⁿ + yⁿ = zⁿ を満たす自然数x, y, zの組は存在しないという定理です。この定理は17世紀にピエール・ド・フェルマーによって提唱されましたが、その証明はアンドリュー・ワイルズによって1994年まで見つかりませんでした。

最近、Anthropicの研究チームが、証明支援システムであるLeanを用いて、このフェルマーの最終定理の形式的な証明を完成させました。これは、数学的証明の信頼性を高める上で画期的な成果です。

Leanは、マイクロソフトによって開発された証明支援システムであり、数学の定理を形式的に記述し、その証明を検証するために使用されます。Leanは、その強力な型システムとメタプログラミング機能により、複雑な数学的構造を表現するのに適しています。

Anthropicの研究チームは、Leanのコミュニティと協力し、フェルマーの最終定理の証明をLeanで実装しました。このプロジェクトは、数年間にわたる多大な努力の結晶であり、多くの数学者やコンピュータ科学者の協力を得て達成されました。

この形式的な証明は、ワイルズによるオリジナルの証明の主要なアイデアを捉えつつ、Leanの論理フレームワーク内で厳密に検証可能な形に落とし込まれています。

フェルマーの最終定理の形式化は、数学の分野におけるAIの応用可能性を示す好例です。今後、より多くの数学的定理が形式化され、証明の信頼性が向上することが期待されます。また、これはAIが数学的発見を支援する新たな道を開く可能性も秘めています。

この成果は、数学とコンピュータサイエンスの境界をさらに曖昧にし、両分野の発展に貢献するでしょう。

［画像: フェルマーの最終定理の証明に関する概念図］