01 / QUICK GUIDE
まず、30秒でつかむ
- 01
Anthropicは9月4日、Claudeがフェルマーの最終定理の証明を、Leanという機械検証用の記述で最初から最後まで書いたと発表しました。
- 02
使ったのは既存の数学者による証明や公開ライブラリーです。新しい証明の発見ではなく、人向けの論理を機械が一行ずつ確認できる形へ直した成果です。
- 03
約1,300万行、約60億出力トークンという大規模な試みです。ただし、この大きさはAIの賢さや効率を示す点数ではありません。
02 / KEY WORDS
専門用語を、やさしく。
ここだけ押さえれば、残りの本文はスムーズに読めます。
- 形式化
- 人が読む証明で省かれた手順まで書き起こし、論理のつながりをコンピューターが検査できる形へ変える作業です。
- Lean
- 数学の定義や証明を厳密に書き、各手順が決められた論理規則に従うかを機械で確かめる証明支援ソフトです。
- Mathlib
- Leanで使える定義や証明を世界の研究者が積み上げた公開ライブラリーです。今回の証明も、この共有資産を土台にしています。
- 公理
- 証明を組み立てる出発点として受け入れる基本ルールです。完成物はLeanで標準的に使われる三つの公理に依存します。
03 / THE FACTS
何が起きたのか
Anthropicは9月4日、フェルマーの最終定理について、初の完全なコンピューター検証済み証明を公開したと発表しました。公式ページに公開時刻はありません。
フェルマーの最終定理は、3²＋4²＝5²のような式が、指数を3以上にすると正の整数の組では成り立たないという主張です。1995年にWilesらの証明が出版されました。
記事内の作業ログでは、最終ルートが証明済みになったのは8月18日2時00分57秒UTCです。11日間の作業終了と、9月4日の発表は分けて読む必要があります。
数十のClaudeエージェントが役割を分け、30,300の途中定理を証明しました。そのうち29,500を最終証明で使い、Leanコードは約1,300万行に達しました。
作業にはClaude Codeを使った複数AIの仕組みと、定理の依存関係を整理する共同基盤Prove2Meを使用しました。人は優先箇所を時折指示したと説明されています。
モデルは市販のClaude Fable 5.1そのものではなく、それとおおむね同等という内部研究モデルです。AIの出力を短い文字片で数えた使用量は約60億トークンです。
Leanが論理を検査し、別の比較器で定理文がMathlib版と同じ意味かも確認しました。数学者Kevin Buzzardも完成物をレビューしています。
ただし、Claudeが白紙から別の証明を発明したわけではありません。Wilesの証明を簡潔に整理した既存の道筋や、Mathlib、先行する形式化計画を使っています。
つまり、何が重要なのか
確認されたのは、Claudeが既存の証明を巨大なLeanコードへ落とし込み、定理文から結論まで機械検査を通したことです。証明本体もGitHubで公開されました。
重要なのは速度の記録だけではありません。AIが研究案を増やすほど、人間だけでは追いつきにくい検証を、同じAI技術で支える道が見えたことです。
04 / THE CONTEXT
なぜ、今これが重要なのか
人向けの数学論文は、専門家なら分かる途中手順を省きます。ところが機械は「ここは明らか」を受け入れないため、定義と論理を細部まで書く必要があります。
フェルマーの最終定理の形式化は、数年かかると見られていました。2024年にはImperial College Londonを中心に、段階的に進める共同計画も始まっていました。
Claudeの初期試行は、全体状況を見失い、協力が止まって失敗しました。定理を地図のように分解し、成果を検索・再利用できるProve2Meへ替えたことで進みました。
これはAIの性能だけでなく、仕事の分け方が結果を左右した例です。複数AIへ大仕事を任せるとき、共有状態と検査工程が必要だと分かります。
05 / WHAT IT MEANS FOR YOU
私たちには、何が変わる？
初心者は「難問を11日で解いた」ではなく、「既にある証明を、機械が確認できる形へ11日で変えた」と捉えると正確です。発見と検証は別の仕事です。
たとえば長い契約書でも、AIに要約させることと、条項のつながりを規則に沿って検査することは違います。今回伸びたのは、後者に近い能力です。
約1,300万行という量だけでは、証明の緻密さや効率は判断できません。Anthropicも、洗練されたMathlibより冗長で、必要以上に長い可能性を認めています。
研究現場では、人が読みやすい説明と機械が検査できる証明を対にする考え方が現実味を増します。形式化だけで、人の理解や第三者の追試が不要になるわけではありません。
07 / NEXT ACTION
今日から、どう動くか
- 01
AIに作らせた資料で、生成と検証を同じ一つの依頼にせず、根拠確認を別工程に分ける。
- 02
長い作業は小さな課題へ分解し、完了条件と依存関係を一覧にしてからAIへ渡す。
- 03
大きな数字を見たら、性能値なのか作業量なのか、比較対象と未確認事項を一緒に記録する。