アンソロピック「Claudeがフェルマーの最終定理を完全証明、Leanで検証」

人工知能（AI）企業のアンソロピック（Anthropic）は、同社のAIモデル「Claude」がフェルマーの最終定理の完全な証明を作成し、定理証明ツール「Lean」を用いたコンピューター検証にも成功した。

暗号資産専門メディアのコインテレグラフが9月4日に報じた。Claudeは11日間にわたり大半の工程を自律的に進め、フェルマーの最終定理として初の完全なコンピューター検証済み証明を完成させたという。

今回の作業では、数学的証明を形式化し、論理上の誤りの有無をコンピューターで確認できるようにする定理証明ツール「Lean」を活用した。

アンソロピックは、今回の成果について、AIモデルが長期間にわたり自律的に複雑な数学証明の作業を担い、その内容を形式的に検証した事例だと説明した。