Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成
AI開発企業のAnthropicは2026年9月4日、AI「Claude」がフェルマーの最終定理について最初から最後までコンピューターで検証できる証明を完成させたと発表しました。
Claudeは11日間にわたってほぼ自律的に作業し、証明支援システム「Lean 4」で約1300万行のコードを生成。
Anthropicはフェルマーの最終定理について初の完全な機械検証済み証明だと説明しています。
Formalizing Fermat's Last Theorem ¥ Anthropic
https://www.anthropic.com/research/formalizing-fermats-last-theorem
(以下略、続きはソースでご確認ください)
Gigazine 2026年09月07日 15時37分
https://gigazine.net/news/20260907-claude-fermat-last-theorem-formalizing/
【AI】Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成 [すらいむ★]
1すらいむ ★
2026/09/11(金) 22:46:38.87ID:OH/7102N2026/09/11(金) 22:56:46.32ID:9udiiEno
これを検証するのも大変そうだ
AIにやらすか?
AIにやらすか?
3名無しのひみつ
2026/09/11(金) 22:58:42.17ID:Y6pLMvXy 機械検証済み証明を完成・・・日本語がワカラン
4名無しのひみつ
2026/09/11(金) 23:04:52.73ID:ieYyS2P0 余白のやつか
レスを投稿する
ニュース
- 町山智浩、具材一種類のローソン「一点突破」弁当に「日本をこんなに貧乏にした自民党を、なんで国民の皆さんは支持し続けるんですか」4 [少考さん★]
- 日銀、1.25%への利上げ決定 2人が反対票 ★2 [少考さん★]
- 【女優】見上愛 もともと「照明さん」志望だった 中2で観劇し直感「将来、コレだ」演出家への夢も [少考さん★]
- 【為替】円下落、一時157円台 日銀利上げ決定も「反対」2票で売り [蚤の市★]
- 「日本一おかき処 播磨屋本店」が2027年3月末をもって廃業 [少考さん★]
- 鈴木憲和農相が退任「本当にありがとうございました」★2 [安倍聖帝★]
- 【高市悲報】ひろゆき「日銀が利上げをした途端に1ドル155円から157円に円安。利上げしても円安ってなかなかヤバいよね。」 [733893279]
- 【悲報】米国「生鮮ジャガイモはよ輸入解禁せんかい!」 高市政権への圧力が強まる [834922174]
- 高市、特に用もないのに緊急訪米へ [709039863]
- ロリ神レクイエム、ガチ炎上wwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwwww [398059782]
- 日銀0.25%利上げ [256556981]
- かなたそに握り潰されるお🏰🦍(・o・;🍬)