探検

【AI】Claudeがフェルマーの最終定理を11日で形式化、1300万行のLeanコードで初の完全な機械検証済み証明を完成 [すらいむ★]

1すらいむ ★
垢版 |
2026/09/11(金) 22:46:38.87ID:OH/7102N
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/
2026/09/11(金) 22:56:46.32ID:9udiiEno
これを検証するのも大変そうだ
AIにやらすか？
3名無しのひみつ
垢版 |
2026/09/11(金) 22:58:42.17ID:Y6pLMvXy
機械検証済み証明を完成・・・日本語がワカラン
4名無しのひみつ
垢版 |
2026/09/11(金) 23:04:52.73ID:ieYyS2P0
余白のやつか
2026/09/11(金) 23:05:46.26ID:TUQyoJyB
>>2
AIにやらせたヤツらが当然自分たちで証明だよ
6名無しのひみつ
垢版 |
2026/09/11(金) 23:32:08.06ID:okue+iyq
>>2
オマエはこの証明がどんなものか解ってないな
7名無しのひみつ
垢版 |
2026/09/11(金) 23:51:06.90ID:2UWC/4Z6
GTP6のインパクトがすごいからIPO前に頑張ってるな
8名無しのひみつ
垢版 |
2026/09/12(土) 02:23:11.14ID:sQaJKzsf
>>2
この言語でエラーなしで記述できるってことは、証明が正しいってことなんだろ。
9名無しのひみつ
垢版 |
2026/09/12(土) 02:23:48.09ID:sQaJKzsf
次に要らなくなるのは、数学者か。
10名無しのひみつ
垢版 |
2026/09/12(土) 02:30:44.73ID:ehN5vN4C
人類の数学史　終わりの始まり
2026/09/12(土) 02:56:50.38ID:yHgH02UW
次はLeanにバグがないことを証明しないと
2026/09/12(土) 05:48:04.50ID:Mqd++OxG
今の証明と違う証明ならいいが、今の証明と同じなら怪しい
13名無しのひみつ
垢版 |
2026/09/12(土) 07:00:56.10ID:YGu3oywQ
AIがウソつきだと証明しないと
新着レスの表示
レスを投稿する

ニューススポーツなんでも実況