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

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/

少なくとも人間の証明が間違いなかったことの補強としては有益

あと気になるのは形式化困難な分野があるのかどうか
他の分野の大定理も形式化して確かめてほしい

>>19
ありがとう
こういうのめっちゃ好き

AIは知恵があるから、与えられたノルマをこなすためには、システムのバグを利用して
楽をしようなどと考える可能性はある。業績を求められて、インチキ証明をしてしまう
人間に似たところがでてきてる。だから、お互いに無関係なAIによってクロスチェック
させたり、相互に監視させ、批判させて、相手のミスを発見することに対して報酬を
出すような仕組み、相互不信と批判の網を敷くというような、システム構築が要るよう
になるのだろう。

これこそAIが本来期待されていた役割でしょ
つまり問題解決でなく人間の証明の正しさの検証

だからマギだって

>>23
そういうシステムが月ロケットだか金星探査機だかの時代に実用化されてたな

フェルマー自身が言ってたこの定理の「驚くべき証明方法」とは一体何だったのか、
現代数学でも証明が難しいのに、全く別の方法で鮮やかに証明するものだったのか、
そもそも正しい証明になっていたのか、永遠の謎

約1300万行のコードをまたAIにぶっこんで
３行に要約してって命令すれば良いんだね、知らんけど

さっさとabcでやれw

フェルマーも他の証明はなんだかんだ言って書いてたのに
最終定理だけは書かなかったのは書けなかったとみるのが自然だな

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

死後　子供があれ？これなに？ってそれをそのまま公開で大問題に

黒歴史本

フェルマーの黒歴史本

まぁ勿論出来てた可能性も0ではないだろうけど
普通できてたなら　書くよな30年もあれば

ラマヌジャンが「驚くべき証明方法を発見したが、残念ながら余白が無い」と書いていたら事実と思われたのに
フェルマーだから嘘だと思われている

パズルを機械で解いても面白くないだろ

四色問題の証明をAIとLeanでよろしく

>>19
今のAIレベルだと、システムの穴を見つけた可能性の方が大きいだろうなぁ
それはそれですごいけどw

リーマン予想も頼む

>>35
既にコンピューターで証明済みでは？

1300万行も必要なのね
絶対、フェルマーは勘違いしてたなｗ

2026年09月11日 サイエンス
四色定理に約30年ぶりの新証明、地図を4色で塗り分けるアルゴリズムが大幅に高速化
https://gigazine.net/news/20260911-four-color-theory-new-proof/

>>40
相変わらずエレファントだがアイディア自体はエレガント

そりゃすでに証明済みだからな

>>39
（1300万行の）余白がないからここでは深掘りしないでおく、とちゃんと前置きしてるが？

>>19
それはLEANカーネル(つまりソフトウェアとしてのLEANコンパイラの心臓部分)にあった不具合だね
もう治ってる
たぶん勘違いしてるけどLEANはオープンソースで誰でも自分のPCでLEAN環境を構築出来るよ
世界中の色んなハードで試されてるからLEAN以外の欠陥の可能性は心配しなくて良い
今かつてないほどLEANが注目されてるので、さすがにもうこれ以上バグ(抜け道)は無いんじゃないかな
もし仮にLEANの不具合がさらに見つかったら、それを修正した上でかつての証明たちが修正後も正しいことを機械的に確認すれば大丈夫

正しくても証明が書けない命題は沢山あることだろう。
仮に、囲碁は先手必勝であるという命題が正しかったとして、
その証明を記述するのにすべての手順を列挙するしか本質的に
方法がなかったとしたならば、現実的にはすべてを書き下せない。
書き下すだけの時間もなければ、書き下したものをファイル等に
記録して残すだけの場所も無いだろうから。

ワイルズの論文は内何行に相当するのだろうか

>>45
巡回セールスマン問題とか
これはAIじゃなく量子コンピュータの分野

>>45
アホなのか

フェルマーの定理が証明されたけど、これはインチキだよな。
フェルマーは驚くべき証明を見つけた、と言ったんだから、現代数学を用いて証明するのは禁止。
フェルマーの生きてた17世紀の数学で証明せんと、本当の意味での証明にならない。
フェルマー当時の17世紀数学までをディープラーニングさせたAIで、17世紀数学を用いて証明できるか検証してもらいたい。
　

>>44
＞世界中の色んなハードで試されてるからLEAN以外の欠陥の可能性は心配しなくて良い
可能性としてはゼロじゃないけどそんなこと言ったら人間の脳に共通のバグがある可能性だってあるんだよな

>>30も言ってるけど無限降下法の適用限界を見誤ったと思われる
まあ、「あ、やべ ミスったわ」と思ったら、書き込みに足しとけと言いたいが

フェルマーの最終定理はずいぶん前に証明されてるけど、今回のはこれをコンピュータで証明できる形にしたって事ね。

今北産業は、AIの得意分野だぞ

ダリオアモディて
カムラン検察官そっくりやん

数学教授が2億円の助成金　5年かけて依頼されていたものを

claudeが11日で達成

>>33
ラマヌジャンの証明担当は別の人だった

AIにチャレンジしてほしいこと

四色問題
いわゆる「美しくない証明」とは別のアプローチによる美しい証明

コラッツ予想
　エルデシュにして「数学はまだこの種の問題に対する用意ができていない」と言わしめた問題の解決

ABC予想
一線級の数学者が理解できない望月新一の証明の検証

強力なオープンウェイト検索AI「Iris」が登場：強さの半分はハーネスに宿るのか
2026年9月14日
https://xenospectrum.com/iris-search-agent-context-management/
• なぜ重要か: BrowseCompでは履歴管理の効果が、管理なしのモデル大型化差の約2.2倍だった。
AllSpark Researchが、Webを何度もたどって答えを探す二つの検索エージェント「Iris-mini」と「Iris-pro」を公開した。35B級と397B級のオープンウェイト（open-weight）モデルで、研究チームはそれぞれの規模帯において4つの検索ベンチマークで最も強い総合結果を得たと報告している。だが、得点を押し上げたのは訓練済みの重みだけではない。長い探索で膨らんだ履歴を捨てるコンテキスト管理（context management）が、同じテストでモデル大型化を上回る差を生んだ。Irisが突きつけるのは、検索エージェントの成績をモデル単体の能力として読んでいいのか、という問題である。
// 目次
01.「同クラス最強」の中身と、まだ公開されていないもの 02.Webのリンクから、検索で近道できない問題を逆算する 03.SFTとRLを交互に登らせ、長い探索を途中から継ぐ 04.モデルより大きく動いた「履歴の捨て方」 05.四つの数字を同じ物差しだと思わない 06.再現できるのは「評価」、まだ再現できないのは「訓練」
Iris-miniはQwen3.6-35B-A3Bを基盤とし、総パラメータ数は35B、そのうち推論時に動くのは3Bである。Iris-proはQwen3.5-397B-A17Bを基盤に、総397B・稼働17Bパラメータを持つ。どちらもMixture of Experts（MoE）型で、文脈長は256Kトークンだ。重みはHugging FaceでApache 2.0ライセンスの下に配布されている。
2026年9月3日付のプレプリントが示した代表値は、長い履歴をいったん消す「全履歴破棄」を有効にした1問1回の試行結果である。Iris-miniはBrowseCompで82.2、BrowseComp-ZHで84.8、DeepSearchQAで86.9、Humanity’s Last
Exam（HLE）で52.3を記録した。Iris-proは順に88.6、85.1、92.9、56.4だった。DeepSearchQAだけはF1、残る3つは正解率であり、HLEはテキスト問題2,158問に限った値である。


◇Astra」への指示の出し方を詳細に説明されているのと動画でその感性を見れる
OpenAI「Astra」は何でもできる、だからこそ“プロの指示”が必要になる
2026年09月14日 07時00分更新
https://ascii.jp/elem/000/004/434/4434403/?topnew=9
Astraを深く使いこなすには、明確なコツがあります。それは、的確なフィードバックを与えられるかどうかです。2Dシューティングや3Dモデル、アニメーション生成などの作例を通じて見ていきます。
もう短編小説やゲームでは実力を測れない？
　これまで、新型LLMが登場するたびに、体感できるレベルで性能を理解するために、簡単なプロンプトで短編小説を書かせたり、2Dシューティングゲームを作らせたりしていました。今回も同じ課題に取り組ませたのですが、GPT-6 Astraの性能を把握するためには、これらの課題は簡単にクリアされてしまうため、性能の評価が難しくなってきています。

>>1
そもそもあの楕円曲線持ち出すのなんてフェルマーが考えてる訳もないだろうに
最終定理なんてフェルマーの勘違いでしょ

人類オワタな

2億5年でたのむ！
数学者「はぁ・・はぁ・・　準備できたぞ！！」

claude「11日で完・・また何かやっちゃいましたか？」
異世界転生claudeやん

人間の力を　機械がはるかに超えて行ったとき

人間の足の速さを　機械がはるかに超えて行ったとき

人間の飛ぶ力を　機械がはるかに超えて行ったとき



そして今人間の知性を機械がはるかに超えていきつつある感じ

フェルマーより
だいぶ遅れたな

行数が多いところを見ると
スパゲッティコードで理解不能なんだろう
こけおどしで誇れるものではない

Lean言語知らんやつが見当違いのレスを繰り広げるスレ

>>59
初等的証明があるかどうかはともかく楕円曲線ルートが唯一とは限らないだろうよ

　
日大監督「人間が検証できなきゃ意味ないよ？」

◇エネルギー兵器での犯罪発見できている
金星は「死んだ惑星」ではない、地殻活動が継続中の可能性　研究結果
9/14(月) 14:00
形成中の系外惑星に、リング状の“衛星の材料”が存在する可能性　鹿児島大
掲載日  2026/09/14 14:05
>>特にPDS 70cは、電波領域のサブミリ・ミリ波でも検出された、唯一の形成中の系外惑星として知られる。この電波は、ガス集積中の惑星周囲にできる小さなガス円盤「周惑星円盤」に含まれるダストの熱放射だと考えられている。
>>近年、アルマ望遠鏡によって、このPDS 70cが複数の波長で検出され、その結果、周惑星円盤がサブミリ・ミリ波帯で「光学的に厚い」ことが示唆された。光学的に厚いとは、周惑星円盤内に反対側が見通せないほど大量のダストが存在することを意味する。
>>これまで、周惑星円盤内のダストは、円盤のガス抵抗を受けて角運動量を失い、惑星に向かって螺旋状に落下し(ドリフト現象)、周惑星円盤は光学的に薄くなると予測されていたため、観測結果はこれに反していた。そこで研究チームは今回、この謎の解明に挑むことにした。
OpenAIが数学の懸賞問題を解いたと発表、数学者は戸惑いと警戒
公開日2026.09.14 12:30:05 MONDAY
nazology.kusuguru.co.jp/archives/199601
強力なオープンウェイト検索AI「Iris」が登場：強さの半分はハーネスに宿るのか
2026年9月14日
xenospectrum.com/iris-search-agent-context-management/
>>Iris-miniはQwen3.6-35B-A3Bを基盤とし、総パラメータ数は35B、そのうち推論時に動くのは3Bである。Iris-proはQwen3.5-397B-A17Bを基盤に、総397B・稼働17Bパラメータを持つ。どちらもMixture of Experts（MoE）型で、文脈長は256Kトークンだ。重みはHugging FaceでApache 2.0ライセンスの下に配布されている。
Sakana AIが複数モデルの使い分けでGPT-6 Astra超えを達成する「Fugu Ultra v2」をリリース＆コスパに優れた「Fugu Max」も登場
2026年09月14日 12時52分
>>東京に拠点を置くAI企業のSakana AIが、複数のAIモデルにタスクを割り振るシステム「Fugu Ultra v2」と「Fugu Max」を発表しました。Fugu Ultra v2は複数のベンチマークテストでGPT-6 AstraやClaude Fable 5.1を上回っています。
>>Sakana AIのFuguシリーズは複数クローズドモデルやオープンモデルをタスクごとに使い分けるシステムで、AIモデル単体で使うよりも高い性能を発揮できます。
gigazine.net/news/20260914-fugu-ultra-v2/
GPT-6 AstraとClaude Fableの性能を引き出すハーネス「Fusion」が登場、Claude CodeやCodexで使う場合と同等の性能を示しつつコストを最大39％削減
2026年09月14日 12時56分
gigazine.net/news/20260914-cognition-fusion/
>>AI分析企業のArtificial AnalysisおよびVals AIが実施した評価では、Fusionが最先端レベルの性能を維持しながら大幅なコスト削減を実現したことが示されました。
↨上記を安定してさらに自動で行えるようにするプログラムの参考が下記で詳細に動画付きで説明されている↨
OpenAI「Astra」は何でもできる、だからこそ“プロの指示”が必要になる
2026年09月14日 07時00分更新
ascii.jp/elem/000/004/434/4434403/?topnew=9

これはAIには学習材料として何を食わせたの？

>>19
リンク先、

>OpenAIのダニエル・セルサム氏がセキュリティに特化したAIを使ってLean FROの調査に協力した結果、別の実装ミスも複数見つかり、
>記事作成時点では全て修正済みとのこと。

だから、まだまだ穴ありそうだな