海外の反応
2026年10月8日
【海外の反応】AIが未解決の数学証明を量産、人間はまだ理解できず議論に
計算理論学者スコット・アーロンソンが自身のブログに書いた「The Mathocalypse(数学終末録)」という記事が、Hacker Newsで議論を呼んだ。OpenAIなどのAIが数学の未解決問題の証明をLean(証明を機械的に検証できる形式言語)で量産する一方、人間側はまだその証明の中身をほとんど理解できていないという内容だ。コメント欄では、Leanによる検証自体が正しく定式化されているのかという疑問、数学者という仕事の意味がどう変わるのか、AIの成果は単なる統計的な力任せの探索に過ぎないのではないかという点で意見が割れた。
数学終末録(ザ・マソカリプス)
出典: scottaaronson.blog / 元記事はこちら
4
海外の名無しさん
2026-10-07 20:54
ピタゴラスの定理の証明だって何十通りもあるはず。目的は単に『証明する』ことじゃなく、普通の数学者にも直感的に分かる、よく書かれたものを作ることだ。深く理解することで、もっと良い問いを立てられるようになる。
6
海外の名無しさん
2026-10-07 20:46
『うちの9歳の息子が母親をからかって「ママ、ロボットがママの一生のテーマだった数学の問題を解いちゃったんだって? ウケる!」と言った』とあるが、普通9歳児がこういう言葉を口にするのは大人の言動を真似ているからだ。嘆かわしい状況だ。
7
海外の名無しさん
2026-10-07 20:27
『しかしほとんど誰も、これらの証明を理解していないようだ』とあるが、OpenAIなどが出した証明を実際に誰かが検証したのか? それともLeanのコードが通ったというだけで、みんな正しいと思い込んでいるだけなのか? Leanのコード自体が間違って定式化されている可能性もあるのでは。
24
海外の名無しさん
2026-10-07 20:28
>>7への返信 AI生成のLean証明の多くが誤って定式化・誤訳されていると主張する論文が出ている: https://arxiv.org/abs/2610.08144
8
海外の名無しさん
2026-10-07 20:13
霧に包まれた山の頂にテレポートされた登山者、という比喩が気に入った。テレポーターが存在してしまった以上、それを使ってもっと多くの頂を目指して探索していくべきだと思う。もうAIが存在しない世界には戻れない。
25
海外の名無しさん
2026-10-07 20:16
>>8への返信 問題は『所有権』だ。AIから得られた知見を分配したり、貢献者に報いる手段が我々にはない。経済活動に関わる記号・数値推論のすべてがAIによって行われる世界に、我々は急速に向かっている。
9
海外の名無しさん
2026-10-07 20:17
『AIがO(n(log n)^2)じゃなく実はO(n(log n)^1.99999)だと証明した』的な話が最近多いけど何なんだ…進歩として敬意を払うべきなんだろうが、どうも引っかかる。機械が前の記録を破るために必要最小限のことしかやっていないように見える。
26
海外の名無しさん
2026-10-07 20:24
>>9への返信 多くの場合その定数(この例では2)は予想される下限であることが多く、そこを下回る結果は注目に値する。理論上の限界を突破したと考えればいい。
28
海外の名無しさん
2026-10-07 20:20
>>9への返信 何度も何度も回せばいいだけだよ
10
海外の名無しさん
2026-10-07 20:27
知性と気質に恵まれて数学者としてのキャリアを歩むのに向いていた人たちは、これから一体どんな問題に向き直うのだろうか?
30
海外の名無しさん
2026-10-07 20:52
>>10への返信 これは記事の中でもある程度議論されていて、ある意味で彼らの目標はこれまでと変わらないと思う。『その事柄を最初に理解した人間になる』ことだ。ただ、理解を示すための重要な手段のひとつを失っただけだ。
31
海外の名無しさん
2026-10-07 20:35
>>10への返信 ClosedAI、XTXマーケッツ、サイモンズ財団がスポンサーのAI推し記事ってことね。
33
海外の名無しさん
2026-10-07 20:33
>>10への返信『これから一体どんな問題に向き直うのか』、それはこの先10年でほぼ全人類が向き合わなければならない問題と同じだ。『経済的な価値が何もない状態で、どうやって食べて、住む場所を確保するのか』ということ。
11
海外の名無しさん
2026-10-07 20:35
とんでもない大発表の後にターミネーター2を子どもたちと観ることにした、というScottの正直さと人間らしさが聞けて良かった。感情というのは面白いものだ。
12
海外の名無しさん
2026-10-07 20:19
皮肉なものだ。ある科学から生まれたものが、その科学自体を食い尽くしていく。
16
海外の名無しさん
2026-10-07 20:14
いやいや。『マスポカリプス』でしょ。ただでさえ大変なのに。
18
海外の名無しさん
2026-10-07 20:11
エージェントがやったのは基本的に統計に基づいたブルートフォースだ。何の理解にもつながっていないので何の価値もないし、むしろこの分野にとって有害だと思う。
41
海外の名無しさん
2026-10-07 20:40
>>18への返信 進化も統計に基づいたブルートフォースだ。だからといって生物学に価値が無いわけじゃない。
42
海外の名無しさん
2026-10-07 20:35
>>18への返信 それはAIがやったことの正しい説明になっていない。
21
海外の名無しさん
2026-10-07 20:54
>>2への返信 10年どころか、コメントの4分の3くらいじゃないか、まあそれもそうだけど。
22
海外の名無しさん
2026-10-07 20:36
>>3への返信 これらの証明がより人間に読みやすい証明への取り組みを駆逐してしまい、生態系へのリスクになるという懸念にも通じる。ただ、こうした証明を編集・注釈して我々に分かりやすく届けてくれる『数学インフルエンサー』が増えるかもしれない。
45
海外の名無しさん
2026-10-07 20:54
>>22への返信 それは結局良いことだと思う。ウィリアム・サーストンが昔から言っていたように、証明そのものが目的ではなかった。これからはより良い説明や、理解・直感を育てるためのツール作りに焦点が移るかもしれない。
46
海外の名無しさん
2026-10-07 20:55
>>22への返信 バイブ数学ってやつだ。
29
海外の名無しさん
2026-10-07 20:53
>>10への返信 どんな質問にも即座に答える機械が存在して、自分たちが仕事を失うとしても、それでも数学を学びたいか学生に聞いたら『学びたい』と答えた。(ちなみに1年以上前からこうなると警告はしていた。)
34
海外の名無しさん
2026-10-07 20:52
>>10への返信 聖職者
35
海外の名無しさん
2026-10-07 20:32
>>10への返信 食料と住居(皮肉)
37
海外の名無しさん
2026-10-07 20:26
>>14への返信 それに、独立した著者たちは結果を実際に理解し、読みやすい論文に仕上げるのに時間をかけていたかもしれない。AIの論文は書き方がかなり雑だ。
39
海外の名無しさん
2026-10-07 20:51
>>15への返信 タスク1と2にはAIはすごく向いているんじゃない? タスク3は人間の直感がまだ必要かもしれないけど、それも2026年にはどうなっているか分からない話かもね。
43
海外の名無しさん
2026-10-07 20:50
>>19への返信 トップクラスの数学研究者たちが、AIの進歩は本物で数学にとって危険だと言っていなかったか? 驚いているのはHNのコメント民だけじゃない。
47
海外の名無しさん
2026-10-07 20:40
>>33への返信 これはおかしな話で、その前に、この状況で得をする一握りの人たちは、シェルターや孤島ではとても守りきれないほど『全人類』の飢えた人数が多すぎることを考えるべきだ。
この話題の背景と論点
スコット・アーロンソンは量子計算が専門の理論計算機科学者で、ブログ「Shtetl-Optimized」で知られる。話題の記事は、OpenAIなどのAIが数学の未解決問題の証明を、Lean(証明を機械的に検証できる言語)上で次々と生成している現状を扱ったもので、形式的には通っていても人間側がまだその論理を追えていない点が核心だった。スレでは、Leanの検証自体が正しく定式化されているかを疑う声(誤訳・誤定式化を指摘する論文へのリンクも紹介された)と、たとえ力任せの探索的手法でも進化と同じように価値があるとする反論が対立した。数学者という職業の今後や、証明より「理解」を育てる方向にシフトすべきだという意見も出た一方、量子計算が専門のアーロンソンがAIの整合性理論まで語ることへの違和感を示すレスもあり、科学的な論点とは別に著者個人への評価が分かれる場面もあった。こうした人物攻撃的なやり取りは記事からは除外している。
※本記事は海外掲示板 Hacker News のスレッド「The Mathocalypse」から抜粋し、編集部で日本語に意訳したものです。訳文の責任は当サイトにあります。
この記事のリアクション
まだコメントはありません。