今日の見方
週明けのAI関連株で連想買いが出るとしても、今回の発表だけで国内企業の売上や利益が増えるわけではありません。見る順番は、数学の快挙そのものより、長時間のAIエージェント処理がどれだけ継続利用され、クラウド・半導体・開発支援サービスの採算に変わるかです。
形式化は、AIが書いた証明を人間が行ごとに読み直す負担を減らす可能性があります。ここはソフトウエアとしての価値がある。ただし、今回の成果は既存の証明を対象にしたものです。新しい数学の発見、短く理解しやすい証明、企業の収益化は別の確認事項になります。
注目ニュース
1. Anthropicが「完全なコンピューター検証済み証明」を公表
Anthropicは9月4日、Claudeがフェルマーの最終定理の証明をLeanプログラミング言語へ変換し、エンドツーエンドでコンピューター検証したと発表しました。フェルマーの最終定理は、3より大きい整数nについて、正の整数a・b・cが aⁿ＋bⁿ＝cⁿ を満たさないという命題です。
投資家が見る点： 「AIが未解決問題を一から解いた」とは意味が違います。今回の市場材料は、既存の高度な数学を、AIエージェントの分業で検証可能なコードへ変換できたことです。モデル性能だけでなく、作業を分解し、状態を共有し、最後に検査する仕組みへ焦点が移ります。
2. 11日間で約1,300万行、最終証明に2万9,500件の定理
Anthropicの説明では、Claudeは約11日間で作業し、途中で3万300件の定理をコンピューター検証可能な形にし、最終証明では2万9,500件を使いました。コードは約1,300万行で、Mathlibの規模の5倍超に達したとしています。
投資家が見る点： 大規模なコード生成は、推論需要が大きくなる実例です。Anthropicは約60億トークンの出力を消費したとも説明しており、計算資源・ストレージ・コンパイル時間が膨らみます。AI関連株では利用量だけを追わず、1つの成果物を得るまでの推論原価と再実行回数を見ます。
3. Lean、Comparator、別カーネルで検証経路を公開
公開されたGitHubリポジトリには、Lean 4.33.1でのビルド、Comparatorによる照合、Rust製の独立カーネル「nanoda」による確認方法が記載されています。証明はLeanの標準的な3公理に依存し、Apache License 2.0で公開されています。
投資家が見る点： 価値の中心は、答えを返すチャット画面ではなく、他者が再検証できる成果物にあります。数理ソフトウエア、研究支援、品質保証へ応用が広がる余地はありますが、公開成果物がそのまま商用契約や継続収入を意味するわけではありません。
4. ワイルズ系統の既存証明を形式化した成果
Anthropicは、今回の証明がフレイ、セール、リベ、ワイルズ、テイラー＝ワイルズらの仕事につながる証明経路を、簡略化したワイルズ証明の解説に沿って構成したと説明しています。2024年から進んでいた人間中心の形式化プロジェクトなどの成果も取り入れています。
株価材料として見る点： AIが数学研究を代替したというより、人間が蓄積した理論とオープンな形式数学の基盤を、AIが短期間で接続したニュースです。日本株への直接材料は限定的で、半導体・クラウド・SI・セキュリティ関連への波及を考える場合も、各社の受注、利用量、粗利、研究開発費で裏付けを取る段階です。
確認しておきたい日程
| 日付・時期 | 確認事項 |
|---|---|
| 2026年9月4日 | Anthropicが完全形式化の成果を発表 |
| 2026年9月7日 | 週明けのAI関連株で、材料の織り込みと物色の広がりを確認 |
| 今後 | 形式化ツールの再利用、外部研究者の利用、AI各社の計算コスト・法人契約への反映 |
関連ページ
- Claude Fable 5.1・Mythos 5.1発表｜長時間エージェントと科学研究
- Anthropic「320兆円IPO」観測｜AI競争と日本株への波及
- Anthropic金融AIエージェント革命｜金融・法務・SaaSへの波及
出典
- Anthropic「Formalizing Fermat's Last Theorem」（2026年9月4日）
- Anthropic GitHub「Fermat's Last Theorem in Lean 4」（証明コード、検証方法、Apache License 2.0）
- Lean公式サイト（Leanとフェルマーの最終定理形式化プロジェクトの説明）