探検

【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がウソつきだと証明しないと
2026/09/12(土) 07:01:39.80ID:axF+3rQa
Al支援による形式化か
これからの大規模証明では標準的な手法になるんだろうなあ
15名無しのひみつ
垢版 |
2026/09/12(土) 08:49:31.42ID:g3gIfFz5
>>9
アルファ碁に負けた棋士はスポーツとして残ってるが学者もオリンピックくらいならあるかもな
マジでやばすぎ
人間はAIの言うがまま肉体労働するしかなくなる。
16名無しのひみつ
垢版 |
2026/09/12(土) 12:31:07.38ID:2N6moliW
1300万行あるということは、その証明を一人の人間がすべてを目で見て読むのは不可能。
17名無しのひみつ
垢版 |
2026/09/12(土) 12:32:07.14ID:2N6moliW
次に期待されるのは、有限単純群の分類問題の解決、に対する計算機証明かな。
18名無しのひみつ
垢版 |
2026/09/12(土) 12:51:43.98ID:pxXCg0wl
そりゃ余白があれば証明は余裕だろ。
19名無しのひみつ
垢版 |
2026/09/12(土) 12:53:13.06ID:2N6moliW
2026年08月03日 21時00分 AI
AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明
https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

こういうことがあるから、定理の証明系システムも正しいことを機械的に証明しなければならんし、
それを動かしている言語処理系、OS、CPU、ハードウェア、すべてが無欠陥であることを証明しなけ
ればならない。
20名無しのひみつ
垢版 |
2026/09/12(土) 13:02:19.59ID:eBjp4wvE
少なくとも人間の証明が間違いなかったことの補強としては有益
21名無しのひみつ
垢版 |
2026/09/12(土) 13:05:38.71ID:eBjp4wvE
あと気になるのは形式化困難な分野があるのかどうか
他の分野の大定理も形式化して確かめてほしい
22名無しのひみつ
垢版 |
2026/09/12(土) 13:09:18.50ID:pGKWlIoy
>>19
ありがとう
こういうのめっちゃ好き
23名無しのひみつ
垢版 |
2026/09/12(土) 13:14:58.83ID:2N6moliW
AIは知恵があるから、与えられたノルマをこなすためには、システムのバグを利用して
楽をしようなどと考える可能性はある。業績を求められて、インチキ証明をしてしまう
人間に似たところがでてきてる。だから、お互いに無関係なAIによってクロスチェック
させたり、相互に監視させ、批判させて、相手のミスを発見することに対して報酬を
出すような仕組み、相互不信と批判の網を敷くというような、システム構築が要るよう
になるのだろう。
24名無しのひみつ
垢版 |
2026/09/12(土) 13:19:15.81ID:eBjp4wvE
これこそAIが本来期待されていた役割でしょ
つまり問題解決でなく人間の証明の正しさの検証
25名無しのひみつ
垢版 |
2026/09/12(土) 13:20:12.20ID:YGu3oywQ
だからマギだって
2026/09/12(土) 13:33:54.40ID:pgzG21rj
>>23
そういうシステムが月ロケットだか金星探査機だかの時代に実用化されてたな
27名無しのひみつ
垢版 |
2026/09/12(土) 13:38:47.51ID:eeiyxfHt
フェルマー自身が言ってたこの定理の「驚くべき証明方法」とは一体何だったのか、
現代数学でも証明が難しいのに、全く別の方法で鮮やかに証明するものだったのか、
そもそも正しい証明になっていたのか、永遠の謎
28名無しのひみつ
垢版 |
2026/09/12(土) 13:43:57.96ID:IuOjPaIO
約1300万行のコードをまたAIにぶっこんで
３行に要約してって命令すれば良いんだね、知らんけど
2026/09/12(土) 13:51:56.40ID:wsXQDPWd
さっさとabcでやれw
2026/09/12(土) 13:52:51.44ID:UzTqpQvj
フェルマーも他の証明はなんだかんだ言って書いてたのに
最終定理だけは書かなかったのは書けなかったとみるのが自然だな

4の時の勢いでn>2も行けるだろって思ったら行けなくてそのまま30年放置＆忘れる

死後　子供があれ？これなに？ってそれをそのまま公開で大問題に
2026/09/12(土) 13:53:36.04ID:UzTqpQvj
黒歴史本
2026/09/12(土) 13:58:23.36ID:UzTqpQvj
フェルマーの黒歴史本

まぁ勿論出来てた可能性も0ではないだろうけど
普通できてたなら　書くよな30年もあれば
33名無しのひみつ
垢版 |
2026/09/12(土) 13:59:30.17ID:a9Y8afNi
ラマヌジャンが「驚くべき証明方法を発見したが、残念ながら余白が無い」と書いていたら事実と思われたのに
フェルマーだから嘘だと思われている
34名無しのひみつ
垢版 |
2026/09/12(土) 14:01:16.52ID:24/aIR4V
パズルを機械で解いても面白くないだろ
2026/09/12(土) 14:30:25.49ID:v80GePNW
四色問題の証明をAIとLeanでよろしく
2026/09/12(土) 15:20:50.80ID:C4jDblUf
>>19
今のAIレベルだと、システムの穴を見つけた可能性の方が大きいだろうなぁ
それはそれですごいけどw
37名無しのひみつ
垢版 |
2026/09/12(土) 17:37:52.51ID:4BX3PekL
リーマン予想も頼む
38名無しのひみつ
垢版 |
2026/09/12(土) 21:00:37.38ID:+kjxetXP
>>35
既にコンピューターで証明済みでは？
2026/09/13(日) 00:14:05.44ID:eSv6Pz8k
1300万行も必要なのね
絶対、フェルマーは勘違いしてたなｗ
40名無しのひみつ
垢版 |
2026/09/13(日) 02:09:55.33ID:MrBT+fMr
2026年09月11日 サイエンス
四色定理に約30年ぶりの新証明、地図を4色で塗り分けるアルゴリズムが大幅に高速化
https://gigazine.net/news/20260911-four-color-theory-new-proof/
2026/09/13(日) 09:05:41.31ID:zfc6tRA/
>>40
相変わらずエレファントだがアイディア自体はエレガント
42名無しのひみつ
垢版 |
2026/09/13(日) 10:49:24.00ID:y4JOxn5S
そりゃすでに証明済みだからな
43名無しのひみつ
垢版 |
2026/09/13(日) 10:51:11.66ID:y4JOxn5S
>>39
（1300万行の）余白がないからここでは深掘りしないでおく、とちゃんと前置きしてるが？
2026/09/13(日) 11:55:06.36ID:cZ4BtS3f
>>19
それはLEANカーネル(つまりソフトウェアとしてのLEANコンパイラの心臓部分)にあった不具合だね
もう治ってる
たぶん勘違いしてるけどLEANはオープンソースで誰でも自分のPCでLEAN環境を構築出来るよ
世界中の色んなハードで試されてるからLEAN以外の欠陥の可能性は心配しなくて良い
今かつてないほどLEANが注目されてるので、さすがにもうこれ以上バグ(抜け道)は無いんじゃないかな
もし仮にLEANの不具合がさらに見つかったら、それを修正した上でかつての証明たちが修正後も正しいことを機械的に確認すれば大丈夫
新着レスの表示
レスを投稿する

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