海外の反応
2026年10月27日
【海外の反応】OpenAIのAIが未解決の数学予想に挑む HNで賛否
OpenAIは2026年10月、自社のAIモデルがヤン=ミルズ理論の存在証明とQCDの証明を自然言語で生成し、Lean言語による形式検証まで完了させたと発表した。あわせて、計算量理論で長年信じられてきた指数時間仮説(ETH)についても、k-CNF式の充足割当てを数え上げる劣指数時間アルゴリズムを示すことで反証したという。海外掲示板Hacker Newsでは、この結果がP対NP問題にどう影響するのか、物理学者だけが詳細公開に慎重なのはなぜか、OpenAIのPR戦略や資金関係への不信感まで、話題は数学的な意義から運営への疑念まで多岐にわたって交わされた。
学術コミュニティと協力し、科学的理解を構築する
出典: openai.com / 元記事はこちら
4
海外の名無しさん
2026-10-26 23:09
「当社のモデルは2026年9月9日にヤン=ミルズ理論の存在に関する自然言語証明を、続いて9月18日にはQCDの証明を生成した。作業の分量と複雑さを踏まえ、Leanによる形式化が完了するまで公開を見送った。ヤン=ミルズの存在証明の形式化は10月16日に完了し、これが本稿で説明する協力体制につながった」――完全にイカれてる
5
海外の名無しさん
2026-10-26 22:50
何十年も未解決だった予想や難問が、2週間に一度のペースでバタバタと解かれていくのは衝撃的だ。すごい時代に生きているもんだ。
6
海外の名無しさん
2026-10-26 21:51
指数時間仮説(ETH)が偽であることは必ずしもP=NPを意味しないのは分かっているが、計算量理論に詳しい人に聞きたい。これでP=NPの可能性についての見立ては大きく変わった?
28
海外の名無しさん
2026-10-26 23:10
「水は濡れている」(P≠NPのこと)を証明しようとしていると想像してほしい。経験的にはほぼ全員がそれを認めているのに、証明を組み立てられる形式論がまだない。そのための有望な形式論の候補の一つが、今回AIモデルによって行き止まりだと示されただけの話だ。
29
海外の名無しさん
2026-10-26 22:51
自分にとってはこれは重要な結果だ。P=NPへの望みがかなり強まったと思う(大多数はP≠NPだと考えているようだが)。いつかAIが現代数学の大きな欠陥を指摘し、公理の修正かまったく新しい理論体系が提案されて、リーマン予想の証明につながる日が来ると信じている。
8
海外の名無しさん
2026-10-26 23:10
物理学者たちだけが情報の全面公開を望んでいないように見えるのはなぜだろう? 物理好きの素人目線だと、標準模型を完成させたという話が今回の成果の中で一番大きいように思えるんだが、違うのか?(※自分はPBS Space Timeを見ている程度のにわかです)
9
海外の名無しさん
2026-10-26 22:56
まあ、これは確かにいつもと違う対応で、批判を無視したとは言えない。でも『猿の手』的なオチになるんじゃないかと勘ぐってしまう。発見のペースがこのまま加速し続けたら、そのほとんどが結局は公表されない、ということになりかねない。
10
海外の名無しさん
2026-10-26 21:40
このタイトルは一番大事な話を奥に埋もれさせている。「指数時間仮説は偽である」っていう話のことだ。
33
海外の名無しさん
2026-10-26 21:51
(リンク先の論文より)「任意のk-CNF論理式の充足割当てを厳密に数え上げる決定的アルゴリズムを与える。これは超多項式だが劣指数時間で動作する」とのこと。
35
海外の名無しさん
2026-10-26 21:56
それ、実は3つある『一番大事な話』のうちの一つにすぎないんだよな!
37
海外の名無しさん
2026-10-26 22:14
この分野に詳しくないんだけど、これってSETH(強指数時間仮説)も偽になるってこと?
11
海外の名無しさん
2026-10-26 22:40
OpenAIはみんなの顔色をうかがうのをもうやめるべきだ。成果をさっさと公開して、手柄は自社のモデルと共同研究者にちゃんと渡せばいい。
38
海外の名無しさん
2026-10-26 23:09
まあ、OpenAI自身もそれが完全に正しいという確信はまだ持てていないんだと思う。
39
海外の名無しさん
2026-10-26 22:42
もう公開はしているよ。並行して数学者を雇って証明を整理させているだけの話。
13
海外の名無しさん
2026-10-26 22:27
この件に関して自分がテレンス・タオ派なのか3Blue1Brown派なのか、まだ決めかねている。控えめに言っても、学術界隈はすでにかなりの騒ぎになっている。これがもう新しい日常なんだろう。
14
海外の名無しさん
2026-10-26 22:54
科学はもう大多数の人間の手の届かないところに行きつつある。特にEUはほとんど蚊帳の外だ。
15
海外の名無しさん
2026-10-26 22:31
継続学習やサンプル効率のようなML自体の課題に、彼らがどれだけの計算資源を注ぎ込んでいるのか気になる。それでどこまで成果が出ているのかも。この投稿のような結果を見ると、近いうちに何らかの『シンギュラリティ』的なものが来るんじゃないかと期待してしまう。
17
海外の名無しさん
2026-10-26 22:21
この証明は単なる3-SATではなく、#3-SAT(充足割当ての数え上げ)に対する劣指数アルゴリズムのようだ。これはかなり強い結果だと考えていいのでは?
41
海外の名無しさん
2026-10-26 22:42
3-SATってNP完全問題じゃなかったっけ?
53
海外の名無しさん
2026-10-26 22:49
そう。これまでは、NPがEXPTIME(指数時間)に真に含まれるのかどうかが未解決だった(あらゆる証拠候補を総当たりすればNPの問題はEXPTIMEで解けるのは自明だが、それより速くできるかは分かっていなかった)。3-SAT(正確には#3-SAT)がEXPTIMEより速く解けると示したことで、これに決着がついた。劣指数といってもごくわずかで、準多項式にすら届いていないが、それでも非常に驚くべき結果だ。
54
海外の名無しさん
2026-10-26 22:46
3-SATはNP完全問題の代表格そのものだよ。
19
海外の名無しさん
2026-10-26 22:51
個人的には、彼らが科学や数学の問題に取り組んで結果を公表すること自体は別にいいと思う。
20
海外の名無しさん
2026-10-26 22:42
証明のアプローチを考えるのに、どれだけ他人のプロンプトを拝借したのか気になる。消費したトークン数についても何も書かれていない。しかもSimons財団を通じて資金を回しているのが得意げで、その財団自体がAI推進派でOpenAIとベッタリの関係だ。ビジネスと政治があまりに生々しくて、成果を素直に喜べなくなる。
21
海外の名無しさん
2026-10-26 22:48
ひどいタイトルだな。もっと面白いコメントが読めるのを期待してたのに、はは!
24
海外の名無しさん
2026-10-26 22:28
『広報チームと協力して、こちらが“頭脳を盗むヒル”みたいに見えないようにする』ってことだろ。
30
海外の名無しさん
2026-10-26 23:11
LLMは、進捗を測る手段さえあれば、複雑で非線形な探索空間を効率よく最適化できるからだ。検証しにくい対象になるほど最適化は難しくなる(不可能ではないが)。
32
海外の名無しさん
2026-10-26 23:10
間違いなくそこが限界だ。AIはデジタル世界では無双できる。Leanで検証可能な話なら、囲碁を打ち破るみたいに問題をねじ伏せられる。でも現実世界とデジタル世界がうまく接続されていない領域では、AIはボトルネックにぶつかる。
34
海外の名無しさん
2026-10-26 22:17
ああ、それともう一つ。『当社のモデルは2026年9月9日にヤン=ミルズ理論の存在証明を生成した』とあるけど、おそらく『質量ギャップ』の部分だけはまだ欠けているはずだ。明らかに、これはミレニアム懸賞問題全部に大振りを仕掛けた結果だな。
43
海外の名無しさん
2026-10-26 22:55
AIがあれば、科学は地道な苦行である必要はなくなる。
45
海外の名無しさん
2026-10-26 22:44
誰も他人に検証を『強制』などしていない。
55
海外の名無しさん
2026-10-26 22:49
別のスレッドで同じことを言ったら、『誰もスマホを持てと強制はしていない』という話に例えられたことがある。先回りして言っておくと、この分野にとって重要な成果だからこそ、コミュニティには検証する動機があるんだ。
47
海外の名無しさん
2026-10-26 23:09
ETHを前提にした論文は、おそらく数千本はあるはずだ。自分の論文にもいくつかある。ただ良い面を言えば、これで一気に未解決問題の山ができたということでもある!
49
海外の名無しさん
2026-10-26 23:00
それを『欠陥』と呼べるのかは分からない。それこそゲーデルの不完全性定理が保証していることだ。とはいえ、一番有名な問題がまさにその実例になったら笑えるな。
50
海外の名無しさん
2026-10-26 22:46
本当にすごい時代に生きてるもんだ。明日起きたら何が起きているか、もう予想もつかない。
51
海外の名無しさん
2026-10-26 22:17
そう、SETHとETHの両方が偽になるということだ。
56
海外の名無しさん
2026-10-26 22:26
それは、ステートメント(そのファイルだけで完結している)を、証明本体(何千ものファイルに分散していて、GitHubでは全部表示しきれない)と切り離して、読者が検証しやすくするための工夫だ。証明自体は別のリンク先にある。
57
海外の名無しさん
2026-10-26 22:22
(リンク先を見る限り)本物の証明はこのファイルに入っているようだ。
59
海外の名無しさん
2026-10-26 22:24
すごいね、ありがとう!
58
海外の名無しさん
2026-10-26 22:29
自分も混乱したんだけど、(末尾に`sorry`が残っている)あのファイルは問題文(ステートメント)だけのようだ。実際の証明はAlgorithmsフォルダ内の大量のLeanコードで、最終的な定理はこちらのリンク先に書かれている。
この話題の背景と論点
ヤン=ミルズ理論の存在証明は、クレイ数学研究所が定める7つのミレニアム懸賞問題の一つで、本来は「存在」に加えて「質量ギャップ」の証明が必要とされる。スレッドではこの点を指摘する声があり、今回の発表が懸賞問題の全条件を満たしたと断定はできない。また指数時間仮説(ETH)とその強化版SETHは、SATソルバーの下限性能に関する未証明の仮定で、計算量理論の数千本の論文が前提として使ってきた経緯がある。これが反証されたこと自体は大きな意味を持つが、スレ内でも繰り返し確認されている通り、直ちにP=NPを意味するわけではない。Leanによる形式検証は証明の論理的整合性を機械的に保証する手段であり、問題設定そのものが意図通りかは別途、専門家による精査が必要になる点は記事本文だけでは見えにくい。
※本記事は海外掲示板 Hacker News のスレッド「Working with academic communities to build scientific understanding」から抜粋し、編集部で日本語に意訳したものです。訳文の責任は当サイトにあります。
この記事のリアクション
まだコメントはありません。