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 余白のやつか
6名無しのひみつ
2026/09/11(金) 23:32:08.06ID:okue+iyq >>2
オマエはこの証明がどんなものか解ってないな
オマエはこの証明がどんなものか解ってないな
レスを投稿する
ニュース
- 「今まで何だったん」堀大輔氏 配信終了後に「ショートスリーパー」表記を削除→「睡眠時間は自由」に変更でネット騒然 ★2 [Ailuropoda melanoleuca★]
- 「POPOPO」サービス終了 開始から約半年 川上量生氏が全額出資 庵野秀明氏、GACKT氏、ひろゆき氏らが取締役として参加 [煮卵★]
- 「逮捕してよ」「露出狂キモッ」 公然わいせつ懸念の声… 水球の選手たちが『上半身裸のブーメランパンツ姿』で渋谷を闊歩 激怒の声 [冬月記者★]
- 【芸能】「やばないか」 名倉潤、『しゃべくり007』での放心姿に視聴者騒然… トイレで途中退出、欠席の異変連発で懸念される体調不安 [冬月記者★]
- 小野田紀美大臣「フロント」から4列目へ 今回は「黒のモーニング」でひな壇撮影 [少考さん★]
- 川口バイク男性死亡、トルコ国籍男に異例の実刑判決 1年6月さいたま地裁「危険な運転」 [少考さん★]
- 【急募】なぜ日本人は「左翼」が嫌いなのか ★2 [339035499]
- 気の迷いでボロ空き家買っちゃったけどくっそ後悔してる
- お前らオープンチャット入るか?
- 【緊急】なんG公認のうどん・天ぷら食べ放題店「小麦晴れ」さん、とうとう4店舗目がオープンしてしまう
- 高市内閣新メンバーの一覧がまとめられるもほぼ全員真っ黒で1.3万いいね [268718286]
- 👊😅👊夜長のまったりダブパンハウス🌃🏡