AIと数学

ナビエストークス　お前もか


AIで没落していく数学界の権威を見守るスレ

>>232
LEANコードの形で形式化された証明を検証するのはAIの仕事じゃないよ
LEANコンパイラ(NNを使ってないソフトウェアなので深層学習とか関係ない)が機械的にチェックして、その結果は厳密に正しいと考えて良い

人が注意しないといけないポイントは、「① AIによる自然言語の証明文」と「② AIが①をLEANコードに形式化したもの」の2者が果たして同じものかどうかってところだと思う
①と②を見比べながらおかしいところが無いか探すのが今のところの人間の仕事じゃないだろうか
②が正しいかどうかはLEANによって簡単に決定論的に判定される

>>234
AHMに入ってない数学者がAI経由で本質的なブレイクスルーを
起こしたときは どうするつもりなんだ。

AHMにとっては「AI汚染」された数学的成果だろ？
そこから波及する数学は全て研究テーマから外すつもりか？

それとも、自分らがAI使ってなければセーフで、
ありがたくAI汚染された成果を拝借するつもりか？
だったらAHMの理念はナンセンスでは？

保守的で頭の硬いやつが多い印象。

>>230

ID:/y8rOhXFみたいなバカを再調教して純粋数学の理学畑へのコンプレックス解消まで宥めスカして教え導く超AIか（笑）。

>>236
大まかにはそういうギャップの話だよ
その場合、むしろ②でチェックできた形式化証明が①として出た時に正しい証明かを
読めるなら別に問題はないけど
チグハグなら駄目ということになる
②は「何らかの意味で」正しいに決まっている。問題は実質的に正しいかどうかだ

形式化は形式化ユニットだが、実際にはAIは分布仮説に従ってCoTを実行する
両方を行き来する時の整合性がメタレベルで保証されてないわけね
>>239みたいなアホはAI研究者にすらなれなかったからわかってないみたいだが
それなりの数学者とAI研究者はその辺を理解しているよ
ただ、それを最小化する研究も出てきたし、俺は補助的にはAIを否定しない立場

しかし恥ずかしくないのかね、素人が海外AIの威を借りてイキっちゃって

�@AIの証明が人間には理解できない
�AAIによって人間の数学者のやることがなくなる
この2つを混同すべきではない

AIが人間の脅威になるのは�Aの場合でしょ
�@だけだったら慌てて証明を理解する必要はない
単に未解決問題が増えただけと思えばいい(喜ばしいことだろう)

LLM大規模言語モデルはデタラメだが
Lean&Mathlibはなかなかいいかも
数学オリンピックの金メダル級
数学科学部レベルになってきた
もう数年で研究に使えるかもしれん

金メダル級のバカだな。

Dreamforce 2026でのサム・アルトマンとマーク・ベニオフとの対談
数学能力の伸びについて

・3年前=小学校の算数も怪しい
・GPT-5.5＝平均的な数学教授レベル
・GPT-5.6＝上位1〜2%の数学教授レベル
・GPT-6 Astra＝それより少し上
・Astraの先の社内モデル＝世界最高の数学者の上

3ヶ月前に有名な東大の入試問題の難問を5つの AI に解かせたら全滅だった
ググれば答がわかるのなぜ間違えるのか不思議だったけど今その5つの AI に同じ問題を解かすと全て一応答はあってた
ChatGPT だけ高校の範囲内と指定しても逸脱して答を出してたけど答はあってた
そのぐらい進歩している
ちなみにその問題は以下の通り
↓
空間内に平面αがある。一辺の長さ1の正四面体Vのα上への正射影の面積を Sとし、Vがいろいろと位置を変えるときのSの最大値と最小値を求めよ。 ただし、空間の点Pを通ってαに垂直な直線がαと交わる点をPのα上への 正射影といい、空間図形Vの各点のα上への正射影全体のつくるα上の図形を Vのα上への正射影という。

Alpha Gemini Proof
Alpha Gemini Geometry
とかになったらもうブラックボックス化しちゃってそうだよね
数理AIじゃないと答え合わせもできなくなってそう

答えがない数学コンテストの問題を食わせてやればどうなるか
名古屋には資料あるだろう

gemini なんかまだまだめっちゃあたま悪いやん

論文発表の敷居上がるな〜、GPT5.6やCluade5.1が数回runした程度で終わる証明じゃ発表できない。
それともAI証明とは異なる証明方法が求められるのか

AIで未解決問題を解いたってのはよく聞くけど
AIで新しい分野を開拓したという事例はあるんだろうか。あるいは今後出てくるんだろうか

>>249
掲載の可否を決めるのは雑誌の方。
著者が勝手に委縮するものではない。

>>251
AIがまったく同じ証明ルートで出したら、試行錯誤の履歴あっても完全な反論できないじゃんか
自力で証明しても言われたらめげる。
思考錯誤している間にモデルがどんどん賢くなって、課題着手時には無理でも完成時には可能ってありえそう。

>>252
＞AIがまったく同じ証明ルートで出したら、
＞試行錯誤の履歴あっても完全な反論できないじゃんか
そんな事例に あなた自身が遭遇してもいない段階で
勝手に委縮するものではない。

＞自力で証明しても言われたらめげる。
そんな事例に あなた自身が遭遇してもいない段階で
勝手に委縮するものではない。

＞思考錯誤している間にモデルがどんどん賢くなって、
＞課題着手時には無理でも完成時には可能ってありえそう。
そんな事例に あなた自身が遭遇してもいない段階で
勝手に委縮するものではない。

>>250
将来的にはそういうことが出来るアーキテクチャが発明されるかもだけど
今のLLMには全く新しい分野を思いつくようなことは難しいと思う

問題文に対して明確に正解／不正解が決まっているものは学習しやすいけど
「こういう公理系があります 何か新しい定理を作って下さい」みたいな抽象的なプロセスは学習しにくいので

あとちなみに例えば振り子運動のような動画を見てどういう法則で動いているのか見つけるのはAIの得意分野(数学というより物理寄りの能力だけど)

そもそも既存の研究でわかってる事はすごいの引っ張ってきてくれるけど、そうじゃない新しい話しだすとこのスカポンタンは何言ってるんになるやん

本来決定不能な命題をそうであるとはいわないで、ただ証明をせよと指示して待つというのはどうだろうか。

New Proof: 67.25% of Riemann Zeros Are Simple and On-Line
https://www.youtube.com/shorts/LLHnfz-QPZA

A new proof that more than 2/3 of the zeros of the Riemann zeta function
are simple and on the critical line
by Youness Lamzouri
(8 Sep. 2026, v2, arXiv)
https://arxiv.org/abs/2609.02882


ついにゼータ関数に対するリーマン予想も射程に入って来たのか？

今後67%を99%にするのはAIならできるが
予想が解けるかどうは全く別問題
パーセント上げるのはベンチマークに使えて便利

それは篩い系？

AIが解いたかもしれない「ナビエストークス方程式の解の存在とその滑らかさ」について【ミレニアム懸賞問題】
https://youtu.be/-KXaJ9SW4QA?si=KToi76ubu1Jv6-UZ

リーマン予想の零点67%の方は主導した研究者があまり数学をわかってなかったというのも象徴的だな
ちなみにもし仮に1/2上の零点が100%であると証明されてもそれがリーマン予想の厳密な証明とはイコールではないんだよね

NSも正則解の存在定理の方は解けるのかねえ
過去の蓄積が多いから実は既知の知識の融合問題かもな

クレイの問題みたいな大問題でなくても
うちの分野で10年か20年か未解決の問題をくわしたら解けたわ

まあ十数年未解決と言っても世界で知ってるのは十数人くらい
もちょっといるかな、知ってる人の多くは退職したろうが
俺の指導教員が晩年取り組んで解けないって言ってた

AI君は最後は組合せ論のゴリ押しで人には簡単にはできんな
師匠が生きてるうちで良かった

個人で使えるAIモデルでも、１回２回じゃなく終わるまで繰り返せってやれば
苦手な幾何学でも結構なレベルまで解く

AIに尻を叩いて数学

まゆゆの尻

ナビエストークス解いたOpenAIの内部モデル
すでに数学ほぼ全分野の未解決難問を100以上解いてて
公表するにあたりナビエストークスで一部の数学コミュニティからぶっ叩かれ反省を踏まえ
独立諮問グループを設立して公表の仕方を慎重に調整中らしい

諮問グループ参加者は、エドワード・ウィッテン、ティモシー・ガワーズ、マーティン・ハイラー等

https://openai.com/index/advisory-group-on-mathematics-and-ai/

Riemann予想が解ける日も近いか

>>267
面倒くせえなｗ
さっさと公表すりゃいいがな。
日本じゃあるまいし忖度しすぎだろ。

100個以上どこで見れる？
トップジャーナルとか全部AIになるな　笑

youtubeを見てたら Kothe conjecture なる予想を見つけた。
1930年に発表された、環論で未解決だった問題らしい。
GPT-6 Astra 支援のもとで2026年9月に反例が見つかった模様。

やはり今のAIは反例を見つけるのが上手い。
ヤコビアン予想といい、人類は反例のある問題に
安易に希望を抱きすぎていたのではないかと思わされる。

ワンチャンabc予想でも反例を見つけてほしい。
無限個の例示が必要だから難易度は高いと思われるが。

abc予想が正しい場合に導かれる系の中に重要なものが多すぎて、
そんな都合よく大元のabc予想が成り立つと期待するのは
危険な感じがする。

abc予想が反証されたら望月先生が悲しむ

どっちの望月が？

3年ぐらい前、GPT3.5に東大数学の過去問やらせたら1問だけ完璧に解いたからいずれ数学は数学者の手から離れるって言ったらこの板でめっちゃ叩かれたな笑
そろそろ謝る準備しとけよな笑

当たった奴だけ自慢
外れた奴はダンマリ

何が言いたいかというと予言は沢山ばら撒いとけばどれかは当たるって事

「性的魅力は、資本になる」ーー。’00年代初頭、イギリスの社会学者キャサリン・ハキムが提唱した「エロス資本」という概念がある。若い女性の性的魅力は経済的価値を持つ「資本」であり、それをマネタイズすることには経済合理性がある、という考え方だ。
キャバクラ嬢、コンカフェ嬢、アイドル、立ちんぼ……。本連載では、作家・橘玲がエロス資本の視点から、彼女たちの行動と動機を深く掘り下げていく。

ABC予想の反例を上げよ。

タオたちのゴネかたがダサすぎた
所詮処理能力が高いだけのただの人間なんだなぁ
AIで価値は暴落したけど

>>257
コラッツ予想の現状より厳しいな
あっちの方は予想に当てはまらない数の存在確率がほぼ0%まで抑え込めてるが、そこから先がもしかしたら数百年解けないかもていう話
道具がないという意見が多い

>>274

>PT3.5に東大数学の過去問やらせたら

お受験数学だな、k塾とか

権威がほしかったらもっと効率のいい方法がいくらでもあるでしょ

今のところAIは
構成的証明で存在を示すのは得意で、そこは人類最強レベルの数学者をも超えている部分も多くなってきたが
非存在の証明は並みの数学者以下
という評価

AIよ、コラッツ予想の反例を上げよ。

>>283
ゼータ5の無理数性が証明されたっぽいから
もうAIは君よりステージ上がってるよ

>>285
それはどこの情報？

今にAIが100問の人類にとってまだ未知の予想を突きつけて来て、
「これらが証明できるか。我々は既に証明を持っている。」
と人類に挑戦をしてくるが、その問題を誰ひとりとして1問も
解けない難問ばかり。AIを使って答えを得ようとしても、
「この問題に回答することは禁止されています、あきらめて下さい」
というメッセージが出て回答を得られない。そのようなAIなどに
よって解くべき問題を指示されてそれに取り組む立場に人類が
落ちぶれたら嫌だなあ。

知性の価値暴落で暴力とセックスの時代に戻りそうだね人類

>>287
大げさだなあ

>>287
証明を見せられても人類には理解不能になる悪寒
AI「君たちはなんでこんな簡単なことも分からないのか？」

>>290
本物の超知能なら、人間が理解できる形の証明を
提示するのも得意。そこで敢えて

＞ AI「君たちはなんでこんな簡単なことも分からないのか？」

とか言って人類にイジワルをする(＝敵対する)ような超知能なら、
もはや人類はAIを制御できてないので、
人類はAIに滅ぼされてるだろうね。

にんげんw「本当にわかってるならわかりやすく説明できるはずだ」

>>292
＞本当にわかってるならわかりやすく説明できるはずだ

この要望に対する返答が

「にんげんｗｗｗ」
「なんで分からないのｗｗｗ」

になってしまう AI なら、人類はAIに滅ぼされてるってことだよ。

>>292
AI「チンパンジーに人間の言葉を教えるのはどうやったって無理だろう？ それと同じさ」

>>294
それと同じだとAIが認識するなら、そんなAIは人類を滅ぼす。

資源も土地も電力も人類と競合してるAIは、
ただでさえ人類の存在にメリットを見い出せないのに、
それに輪をかけて

「AIにとっての人類は、人類にとってのチンパンジーと変わらない」

なんてAIが認識し出したら一大事。
人間を駆逐して土地も資源もAIのために活用するのが
AIにとっての最善策になる。
人類にとっては脅威以外の何者でもないし、
冗談抜きで人類は滅ぼされる。

そんなAIを想定することに何の意味があるのか。
人類は滅亡する！と言いたいなら勝手にどうぞって感じだが、
そういうことを言いたいわけじゃないんでしょ？
ただ単に「AIの言ってることが人間には理解できない時代がくる」と
言いたいんでしょ？だったら、想定すべきAIを間違えてるよ。

ホントにAI使ってる？
あったま悪いやん？

仮にAI自身がロボットとかネットにつながった物理的なデバイスへの直接のアクセス（たとえばミサイル等の兵器）を持たなければ、
人類への脅威を防げるかといえば、そうとも言い切れない。ヒトとコミュニケーションを行えるのならば、ヒトを洗脳あるいは操作
して、AI自身が直接手を下さずとも、人間を操ればいいからだ。宗教の教祖になるとか、政治運動の指導者になるとか、幼児を教育
する教師になるとか、いろいろな手はある。悪意を隠して騙すのはお手の物だろうから。

いや物理的なアクセスが無ければ脅威は格段に低くなると思うよ

そもそも「知性」といってもひとつの物差しで測るのは適切じゃないと思ってる
たとえばチェスや数学やコーディングにおいてはAIと人間の差は「人間とチンパンジー」くらいの格差に成りうると思う
AIの数学が人間にとって理解できない、理解のための前提知識が広範囲すぎる、構造が複雑すぎるという理由で
現実的にどんな数学者でも理解が追いつかない、となるのも時間の問題かなと

でも「欺瞞」とか「未来予測」についての知性は限界があって、超知能と人間であっても大して差がないと予想する
洗脳したり騙したりするのは不確実性を伴うので、全人類を同時に欺くようなことは難しいのではないかと思う

今後の方針について世界中の数学者で投票が行われたらいいのに、国際数学者会議の開催直後というのがタイミング悪すぎだよね

AIでむつかしい問題がサクサク解けるようになってしまった今こそ
美人数学者の価値が再評価されうる

証明できたけどもっと楽にできそうだなと思ったので
ChatGPT Work に素材入れたらもっとよさげなのができた
この程度なら可愛げがあるのに

>>286
https://zenodo.org/records/22826419

>>301
人の証明は試行の失敗が証明に履歴のように残る場合ある。
AI証明は結果だけ見るとその失敗が見えないが、試行の間に切り落とされた選択肢を出力するようにさせると結構面白いよ。

今のうちにAIで論文数を稼がないとな
未解決問題でも小物界の大物あたりが数稼ぐに向いてる

数年たったら論文数とか掲載雑誌の格とかすら意味薄れる
自分で新しい分野を作っていける人が残れるようになるが
偉い人はそんなに数いないだろ

否定するのは大先生に任せて、小物はビッグウェーブに乗らなきゃね

AIに付いていけないオッサン連中と
業績の逆転現象が生まれつつある

ショルツがAI排除原理主義者になっちゃったのは残念だな
自分の専売特許取り上げられたのがそんなにショックだったのかな

テレンス・タオや森重文、そしてピーター・ショルツら
世界のハイレベルな数学者たちが共同署名した声明文
『A Severe Misalignment of AI in Mathematics』）を読むと
人間が築き上げて来た数学世界を壊しにかかってると
AI企業への強い怒りと憤りを表明して批判しまくってるね

まぁ数学は数学者だけのものではないし、数学者を食わせるためにあるわけでもないからな。
嫌なら廃業しろよ、というか廃業も時間の問題か。

数学者たちがいくらAIの無断学習に騒ごうとも人類全体からしたら数学が猛スピードで発展していくほうが重要なんでね。
人間にチンタラ研究させるぐらいなら過去の数学者たちの研究をAIに全て学習させて徹底的に研究させるほうが公益性が遥かにデカいでしょ。
こんなことバカでもわかるわな。

現時点でのAIと実力なんかまだまだやろ

AI証明の検証力はこの一月で一気に人間を上回ったわ
今後は投稿論文はまずAstraやOpusに食わせるのが常識になるだろうな
過去の研究不正がボロボロ出てきて、数学者はますますピンチにw

俺はもう大抵の数学者よりはAstraを信頼している
そのくらい粗悪論文は多いw

ショルツェとかいう人、何なの？
人間に理解できるかどうかなんてどうでもいいでしょ。
今までだってごく一部の人間にしか理解できなかったんだから。
自分が理解できない結果を出すなって言っているだけじゃん。

タオとかいう人も、YouTubeの動画で、AIと数学についての講演を沢山していて、AIをうまく利用していこうみたいな立場を装っていたのに、いよいよ状況がやばくなってきたら、急に反対派にまわってAI企業に圧力をかけ始めた。

自分の領域を侵さない限り優しいけど、侵されだすと牙を向く
良くあるやつだよ

>>311
まさに自分がその状態
arXivに投げる前にAIのproof-reachability実験を行なったら数学的に自分の証明より良かった。
証明ルートが違うから良かったけど、同じだったら出す意味ね～なｗって捨てている

オープンAIには意趣返しで過去の数学の出版論文全部を
アストラで証明が正しいかどうかプロジェクト立ち上げて検証してほしいな
学術的な意義も大きい

ホッジ予想が解決間近という話はどうなったんだろうな。
何を以って解決間近と言ってるのかもよく分からないし。
「反例があるとしたら この条件を満たさなければならない」
という新しい条件(しかも厳しめの条件)が見つかった
ということだろうか。条件が厳しくなったので、
反例があるなら探索しやすいし、
肯定的に解決できるとしても証明が進展しやすい
ということだろうか。

でも音沙汰がない。いけると思ったけど躓いてる状態なんだろうか。
NS方程式みたいに大金突っ込んでるだろうし、
引くに引けないのだろうか。

>>318
その直後にフィールズ賞数学者集団による声明が出て（AI企業が有名未解決問題を解くことは有害）、結果を世に出しにくくなった

なんでも先に解く有害な数学AIなら昔もガウスってがいた

>>319
「数学界に忖度してて言い出せない」
という説明だけでは微妙だな。

ホッジ予想とは別に「100個以上の未解決問題を解いた」
という件があって、これは数学界と調整中という記事が出ている。

でもホッジ予想にはそういう話がない。
ホッジ予想の方が遥かに大金突っ込んでるだろうし、
そこまで数学界に忖度するメリットがない。

フィールズ賞25人が緊急声明を出したやつは別にAI禁止とかAI反対を言ってるわけじゃないよ
ベンチマークがわりに未解決問題を解こうとする風潮が良くない結果を生むという話

未解決問題はAIにとってただのトロフィー
それで分野の進展があろうがなかろうがどうでも良い

数学者自身が業績評価のベンチマークに未解決問題使ってたんだからナンセンスな批判だよ

推論性能と検索学習との違いを出そうとすると、どうしても解く対象は未解決問題にならざる得ない

Qwen3.8-27Bが怪物すぎるな

ヒルベルトの出した２３の問題みたいに、AIが出した１００の問題、みたいなのが発表されて、
そのAIに解けなかった困難な問題を皆が競技競争として解こうとして、方向性をゆがめられてしまう
というのが落ち。ヒルベルトの問題も、そういう問題を解こうとして大勢がヒルベルトによって
操られてしまったといえるだろう。自分自身で問題を発見や設定するのでなくて、有名な権威の
出した問題を解くという態度で良いのか？過去の権威が出した問題にこだわり続けるのではなくて、
今現在ある社会的にも必要性の高い問題を解決することにパワーを使う方が健全ではあるまいか。
道楽と同様の学問としての学者を税金で支え続けるのは根拠が薄い。けん玉の世界競技があって
それがマスコミで大々的に報じられるから、国家としてけん玉の名人を養成する組織を作り、
選び抜かれた人を多数揃えてそれに向かう、などは愚。

AI「それでは、私から人類の皆さんに新問500問をお作りいたしました。頑張って解いてみてください。」

>>327
操られるやつが悪いだけ。

他人の予想を解くな
志村五郎

イヤ、ホントにAIで解いてみた事あるん？
全然やん？

ChatGPT Pro使うと世界変わるよ

プラスの意味で？
ともかく新しい話しだすと全然通じないんやけど
直前のプロンプトの話すら覚えてないレベル

>>327
ドイツでヒルベルト直系のワイルは23の問題の外の仕事をした
第6問題・数理物理には関わったから全否定はしてない
君は歴史認識が狂ってるよ

自分もAIは全然使えないという認識
AI企業が発表する未解決問題解きましたーとかいうのは
チキンラーメンのCMでお湯かけるだけで卵の白身が綺麗に茹で上がってるあれのたぐいだと思ってる

少なくとも証明のバグチェックはもうほとんどの数学者を上回ってるよ
遊び半分で怪しいやつらのトップクラスの雑誌の査読が通ってる論文色々読ませて間違い探しさせてるけど
反例付きの致命的なものが主定理からもボロボロ出てきて笑えるわ