AIに学者の仕事が奪われる! Googleの数学証明AIが50年来の未解決難問を一気に9件証明www

1 : 2026/05/31(日) 10:48:00.62 ID:PSsXu4F+0

Google DeepMindは2026年5月、大規模言語モデル（LLM）と定理証明支援系「Lean」を融合させた形式証明探索AI「AlphaProof Nexus」を発表した。本システムは、LLMの生成した証明ステップをLeanで厳密に検証し、エラー修正を繰り返すことで、ハルシネーションを排した絶対的に正しい証明を自律的に構築する。

本AIは、56年間未解決だった2件を含むエルデシュ問題9件や、未解決予想44件を解決した。異なる数学領域を結合させる独創的な解法は数学者からも高く評価され、1問あたりの推論コストは数百ドルに抑えられた。同時期にOpenAIのAIも別のエルデシュ問題を解決しており、AI開発競争が数学の難問解決という形で表面化している。

この成果は、数学研究にパラダイムシフトをもたらした。これまで天才のひらめきに依存した数学的発見が計算リソースで管理可能になり、AIが問題定義の誤りすら修正し、人間は高次元の概念探求に集中するという新たな協調関係が生まれつつある。一方で、AIによる証明の量産は既存の査読システムを機能不全に陥らせ、発見者のクレジットを巡る論争を招くなど、学術コミュニティに制度やルールの再考を強く迫っている。

【さすがのグーグル】GoogleDeepMindの数学AI、50年来の未解決難問を一気に9件証明

Google DeepMindは2026年5月21日、AIを用いた形式証明探索システム「AlphaProof Nexus」に関する論文を公開した。大規模言語モデルと定理証明支援系を組み合わせ、長年未解決だったエルデシュ問題9件を自律的に解決...

2 : 2026/05/31(日) 10:48:11.67 ID:CZ1engfe0

長くて読めない

3 : 2026/05/31(日) 10:50:12.47 ID:BB1tuKsSd

人はもう終わりということ

4 : 2026/05/31(日) 10:50:19.31 ID:JadHXT5D0

数学者とかAIに絶対勝てないやろうしな

5 : 2026/05/31(日) 10:50:54.61 ID:4RSAZSh/0

数学者はオワコン

6 : 2026/05/31(日) 10:50:55.26 ID:L68TtMPod

哲学の難題もAIによって解かれる日は来るのか？

16 : 2026/05/31(日) 11:21:36.39 ID:mUbcA5T40

>>6
哲学に難問なんか一つもないぞ
単なる言葉遊び
だから文系なんや

21 : 2026/05/31(日) 11:26:36.13 ID:OslAIfiI0

>>6
哲学は問題を解くことが目的ではなくて潜んでいる問題を定式化することが目的やな

27 : 2026/05/31(日) 11:42:09.23 ID:mUbcA5T40

>>21
単なる言葉遊び
西尾維新がまさに哲学

7 : 2026/05/31(日) 10:51:51.46 ID:r5VqHpyPH

しかもまだAIなんてやっと立ち上がった段階やんな
今は世界中の人が幼児段階のAIを育ててて、更なる成長確実で

8 : 2026/05/31(日) 10:52:12.82 ID:9bmh8Xv10

この記事を読んで数学者がAIに取って代わられると認識した奴はおそらく高卒以下なんやろね

9 : 2026/05/31(日) 11:01:37.90 ID:PUsD8o9c0

>一方で、AIによる証明の量産は既存の査読システムを機能不全に陥らせ
これよな
証明したというのは自由だがその検証に膨大な時間かかる

10 : 2026/05/31(日) 11:04:51.19 ID:Nm/BdVKI0

>>9
ワイの会社みたいで草
アホ社員がAIで提案やら改善やらプログラム大量に作ってきて
それを検証証明できる一部の有能社員が擦り切れはじめておるわ
どう考えても有能社員が提案改善したほうが効率ええのに

11 : 2026/05/31(日) 11:10:53.25 ID:2PSRZeVJ0

>>10
アメリカだと既にAIの方が高く付くから人を雇う方に回帰しだしてるのに日本は何周遅れだって話よな
なんG民ですら未だにAIで仕事が無くなるとか喚いてる

13 : 2026/05/31(日) 11:17:51.05 ID:r5VqHpyPH

>>11
んなわけないだろw
アメリカの大手企業のAIリストラの記事が連発してるやん

14 : 2026/05/31(日) 11:20:21.71 ID:J8QCdmKg0

>>13
ちょっと前やな
今は社員がAIクーポンで数千万円使いやがった
という記事がで始めてる

12 : 2026/05/31(日) 11:15:43.56 ID:nxXYOfLb0

プログラムの現場だとAIで作る速度は上がるけど使う側の経験値がないとゴミができるだけだな今はまだなのか5年したら変わるか知らんけど

15 : 2026/05/31(日) 11:20:33.98 ID:Q8AzeibO0

ほったらかしだった証明問題でしかないのでは
やろうと思えば証明できるような問題だったのでは？

17 : 2026/05/31(日) 11:22:37.97 ID:2N/LSn190

証明を検証してるエンジンはLeanてやつなんやな
どれくらい汎用性あるんやろね

18 : 2026/05/31(日) 11:23:00.48 ID:yyZB6U9A0

ヒトカスは無価値

19 : 2026/05/31(日) 11:23:47.28 ID:AyVPVbXb0

学者は解雇で

20 : 2026/05/31(日) 11:26:24.82 ID:CK3HcyC20

事務作業系は負担が減ってアメリカはレイオフ始まってる

22 : 2026/05/31(日) 11:29:50.50 ID:qloTk0fud

AIはプログラム作らせるとフェルマーみたいな嘘つきが多いけど数学界ではちゃんと仕事しとるんやな

23 : 2026/05/31(日) 11:31:33.82 ID:J8QCdmKg0

スターバックスの在庫AIシステムが
適当にやり始めたので
AIの方をリストラしたの好き

割と適当に答えるよなあいつら

28 : 2026/05/31(日) 11:42:18.93 ID:C+pF3gve0

>>23
草
人間味あってええやん

29 : 2026/05/31(日) 11:43:03.44 ID:mUbcA5T40

>>23
わかりません
がいえないからなAIは

30 : 2026/05/31(日) 11:44:10.31 ID:yBtfYI1e0

>>29
プロンプトちゃんと組んだら言えるぞ

25 : 2026/05/31(日) 11:35:48.51 ID:OslAIfiI0

LLMの吐き出す非論理な提案→Leanを用いた論理的に検証→以下ループ

てやり方なんやなこれ
LLMは霊感を得た詩人みたいな役割か

31 : 2026/05/31(日) 11:44:33.77 ID:UDUTYZSr0

AIが出た時に「これはなくならんやろ」て言われた仕事から価値がなくなっていきそう

32 : 2026/05/31(日) 11:45:49.26 ID:EFUl1PeI0

数学・物理学こそAIが強い分野やしな
これから人間が理解できないけど技術的に色々できるようになったというフェーズに入ってくるんやろな
すでにそうなってるけど