フェルマーの最終定理を端から端まで機械検査できるLean形式証明が完成した。Anthropicによると、Claudeを中心とするAIエージェント群が11日間で構築し、Leanカーネルに加えて照合器と独立カーネルによる検査を通過したという。
自然数の命題をLeanの型と論理へ変換
Anthropicは、完成した成果物をフェルマーの最終定理に対する最初の完全なコンピューター検査済み証明と位置づけている。Claudeは11日間にわたり主に自律的に作業し、人間向けの証明をLeanが判定できる形式へ置き換えた。
証明対象は、3以上の自然数nと正の自然数a、b、cについて、aのn乗とbのn乗の和がcのn乗に等しくならないという命題である。Leanの証明支援系は、曖昧な文章ではなく型と論理規則で記述された各段階をアルゴリズムで検査する。
定理グラフが数十のエージェントの作業を接続
数十のClaudeエージェントは、必要な概念の定義、中間定理の証明、証明済み定理を使った上位定理の構築を分担した。初期の試行ではエージェントがプロジェクト全体の状態を見失ったため、共同形式化基盤prove2meが作業状態の共有を担った。
prove2meは定理文を有向非巡回グラフとして保持し、未解決の定理と利用可能な依存関係をエージェントに示した。定理文と証明を別ファイルに分けてリンクを管理する構成がコンパイル負荷を抑え、各定理の自然言語による説明が証明済みの結果の検索と再利用を可能にした。
約1300万行がWilesらの証明経路を形式化
完成した成果物は約1300万行のLeanコードに達し、最終的な証明経路では約2万9500件の中間定理が使われた。証明の数学的な骨格は、Frey、Serre、Ribet、Wiles、Taylor–Wilesによる議論をたどる。
人間からの数学的入力は、優先して扱う対象を指示する時折の高水準な助言に限られた。各エージェントが下位の定理を成立させ、その出力を依存グラフ上の次の定理へ渡すことで、個別の証明が最終命題まで接続された。
Leanと二つの別経路で証明成果物を検査
Lean 4.33.1によるゼロからのビルドでは、成果物の全6万475モジュールが構築された。最終定理が依存する公理はpropext、Classical.choice、Quot.soundの3つと表示され、成果物のモジュールからは未証明部分を許すsorryなどの指定された構文が排除された。
comparatorは、証明された命題と命題中の定数をMathlibだけで記述した検査課題と照合し、同じ命題であることと許可外の公理を使っていないことを確認した。さらに、Rust製の独立Leanカーネルnanodaが同じ環境から書き出した105万2234件の宣言をエラーなしで受理し、Lean標準カーネルとは別の検査経路が加わった。
進行中の共同形式化とは別の完全成果物
Imperial College Londonが運営する別のオープンソース事業は、フェルマーの最終定理のLean形式化を現在も進行中の複数著者プロジェクトとしている。今回の成果物はこの事業そのものの完了ではなく、AIエージェント群が別の証明経路を終端まで接続した独立の研究成果物である。
機械検査は、形式化された命題が指定された公理と定義から導かれることを保証する。一方で、中間定理の名称が人間の想定する数学的意味と一致するかは自動的には判定されないため、成果物では名称よりLeanの定理文が権威ある記述とされている。