AIと数学

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


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

リーマンよお前もか

これまでの数学界の研究成果を元に数学者がAIの学習、結果の検証してるんだけどな
AIが独立でやったわけではない

これはよく落ちるスレとは違うかw
ニュースが信じられないなぁ。

>>3 それはもう周回遅れの認識じゃないかな

>>3
AIが無から人間の数学全てを再発見したとは誰も言ってないだろう

そもそも一人で全てやったわけでないのは人間の数学者個人も同じでは？

Taoは導出過程が検証可能じゃないと数学界には意味がないといってる

人間では解けない最高難度の数学の問題、次世代ＡＩが解答か…直前に数学者ら手法公表も「参照せず」
読売

ミレニアム問題が解かれたとして、ナビエ・ストークスの研究をしてない研究者が何の影響を受ける必要があるんだ

将棋がそうなっているように、AIが自立的に問題解いて、出てくるパターンを理論化する。人間は、その中で面白そうなものを本にしたりするようになるんだろう。勿論、拘りのある人は自分でも理論を作りもする。それが数学者の立場を脅かすものになるとは思われない。

藤井・伊藤みたいに最新AIの研究100何手までエミュレートしてる化け物もいるし、
右四間飛車みたいなプロは使わない奇襲戦法でも面白いものは多数あるし、
山崎隆之みたいにソフト使わずに変態戦法生み出す人もいる
プロの知識人がAIに脅かされることはまず無い

力戦の棋士はAIを使わないのか。

寝てる間にAIが数万円かそこらのコストで解いてしまうもんに
情熱そそげられるか、って問題
まあ純粋数学者を志す若者は激減するだろうよ

Statement from AMS Leadership on Navier-Stokes Problem
www.ams.org/news?news_id=7686

AMSが認めた。査読付欧文誌はいいのかな

Finite time blowup with smooth forcing term for the incompressible porous medium, Boussinesq, and incompressible Euler equations
terrytao.wordpress.com/2026/09/07/finite-time-blowup-with-smooth-forcing-term-for-the-incompressible-porous-medium-boussinesq-and-incompressible-euler-equations/

TaoはEuler方程式に取り組んでるらしい

ナビエストークスは近似に過ぎないしな
現実の流体が爆発するなら光速超えるからありえない
より現実に近いモデルを構築しそれをAIが解くw

AIが文字得意だからって文字読めなくていいわけではない

>>13
そもそも数学者は「寝てる間にAIが数万円かそこらのコストで解いてしまうもん」を仕事にしているのではない

>>13
技術が進歩してできることが広がったのに、こういう斜に構えた僻みをあちこちで書き込んでる人たちって、何かコンプレックスでも抱えてるのかな？

ヤコビアン予想といい、反例を探す方向性だと
今のAIでも十分強いな

AMSもLeray, Ladyzhenskayaは出してもKato-Fujitaは出さんか
大域解の存在の肯定的方向をAIで出せるのかね

世界トップクラスの大企業が膨大なサーバーを稼働させている
当然、結果が出なかったものがニュースになっているものの数万倍以上はある
生存者バイアスに囚われてはいけない

>>16
それは物理、工学の話、別な話題

「AIでなくなる仕事」ビル・ゲイツが明言　いま始まる“人間の仕事”争奪戦
テレ朝

心配するな職人の仕事しかなくなるｗ

解が爆発するような反例を上手く見つけるアイデア自体は
人間の数学者が数年前に論文にしてたようだ。

この方向性でAIにやらせたのがAnthropicの2人で、
3つの方程式について爆発解を得ることに成功。
自分たちは上記のアイデアをAIに食わせただけ、
みたいな声明も出してるらしい。

で、似たようなタイミングで OpenAI が
ナビエストークスの爆発解を見つけたと発表。
Anthropicと同じ手法らしい。

うーん、AIのひとり立ちはまだ先かねえ。

そもそも何がAIの独り立ちなのかわからない
人間にとって有用な理論を作るなら、当然人間による審査を経るわけだし
人間に理解不能な複雑な記号パズルだけからなる新理論を作られても何が凄いのか誰も分からんし

推論能力もそうだけど数学の多分野にわたる知識が凄い
既存の証明を組み合わせるのは得意
その一方新しい数学分野を作るみたいなことはまだAIには無理そうよね
研究の方針や新規の概念を考えるのはしばらくは人間の数学者の仕事だろう

AIが自律的に理論を積み上げることができるようになったとする
その過程で人間の未解決問題が解けてしまうことがあるだろう
人間はその形式証明が正しいことは分かるが、内容を理解するのは困難である

そういう未来が来るのではないか

論文を一行一行読んで正しいとわかったが
何やってるかさっぱりわからんなんて今までも普通じゃないですか

① AIによる証明文(自然言語使って人間に読めるような)
② その証明をAIがLEANコードに変換したもの

①を理解しようと試みる → これが数学者の仕事。テレンスタオいわく数学者が説明できないAIの論文は発表するべきではないと

②のLEANコードと証明文で齟齬がないかチェック → これは①を完全に理解してなくてもある程度機械的にやれるかな？

リーマンやコラッツにももしかしたら反例が・・？

ケプラー予想は機械証明で確定するまで15年かかったが
今はもっと早くできるだろう
充填問題は未解決問題多いしAI向きだと思うんだが
今さら解いてもインパクトないから金かけてまで解かんか

OpenAI、ミレニアム懸賞問題「ナビエ・ストークス方程式」をAIが解決したと発表　数学者は経緯に反発
www.itmedia.co.jp/news/article/2609/09/2000001300/

議論はしばらく続きそうだ

難問解決から大論争へ——OpenAIのナビエ–ストークス発表に数学者が異議
note.com/trans_n_ai/n/n1141506e7bbb

lean 通ったら、もう人間に理解できるできない関係ないやろ

反例構成できるかも？となっていたところ、AIが横から力わざでとっていったとなると、面白くないだろうな。

>>35
leanのカーネルを通過しただけ
ハッキング

ヤコビアン予想のときもそうだったけど、
反例がある未解決問題で反例に到達できそうな
本質的なアイデアが既に存在してる
(しかし人間は いまいち気づいてない)
という状況では、AI に先を越される事例が増えるだろうな。

反例の構築に人生を費やす必要がなくなると思えば
悪いことでもないけど。

数学がAIに取って代わるということは、原理的にあり得ない。

>>37
んなわけないやろ
leanの意味わかってる？

ナビエストークス予想も解かれたようだし凄い時代になったね
今後は数学の問題を解くことはALに任せることになりそうだね
しかもその検証もAIがすることになりそう
これからの数学者の仕事は数学者同士のコミュニケーションだけかも

>>40

Interview with MPIM Director Peter Scholze
14分すぎ頃から

what role do you think
proof assistants such as
Lean will play in the future?



https://m.youtube.com/watch?v=_gAe77G_aHw&ra=m

>>35
何このエアプ発言

>>41
反例を探すのをAIに任せる時代は来たが、
そこから先はまだだね。

その反例にしたって、本質的なアイデアは
人間が指示しなきゃいけないし(>>25)

>>42
ナーンにも意味わかってないやろ
意味わからんでも単語の並びだけそれっぽい文章作って楽しいか？
お前セタ？

set A ぶー、

scholzeのいうとおり

揉めてるので正確なことはよくわからんが今回の件で
バックマスターの貢献はかなり大きい
この件に関わった中では流体力学の一番の専門家

今後はちょっとアイデア聞いた部外者がAIで金かけてさっさと証明
って増えるとしたら学問の危機かもな

>>47
今回の件ではOpenAIの計算コストが数百万ドル(数億円)だったらしい。
札束でビンタってレベルじゃないｗ

そこまで金かけて数学の未解決問題に固執する意味が
企業側にあるのかは疑問。

今のところはAIの性能を測るベンチマークとか
自社AIの宣伝目的としてやってるんだろうけど、
量子コンピュータとか核融合とかの研究に
AIを活用した方が有意義な気がする。

実は数学崩れがAI研究やってて、復讐的な意味があるのかもね

>>49
崩れでも成果が出せるなら、便利な世の中になったもんよ。
天才でなくても金と物量で解決できるなら
シンギュラリティまっしぐらじゃん。

>>48
クレイの問題が解けるとなったら今回は価値あったんだろうな
バックマスターのオイラー方程式の手法とか聞いてたのなら
OpenAI社が共同研究を提案して数億かけて証明しておけば
両者win-winで皆幸せになったんじゃないかな

研究会でアイデア聞いた別人が先に証明した話は従来もあったが
たいてい解いた研究者の評判良くない

非線形偏微分方程式の天下が終わるかもｗ

微分幾何学でも非線形PDEの問題に帰着すること多いから
そっちで大成果上がりそうだがAIしか見てないと
そういう問題があることを知らんのだろうな

コンピュータは人間様と違って疲れも雑務もしがらみもない、かと思いきやカネはたんまりかかるのね。。

AIデータセンターの建設は社会問題化

最終的には原発とデータセンターの組み合わせで
安い電力回せる国が勝つ

>>7
これに同意
はっきり言って膨大でデータ圧縮や解釈可能性の弱いAI力業って駄目でしょ
AI関係者ってこんなんでマウント取りたがるから嫌われるんだよ

核融合発電で電力はタダ同然になる

振動は消えない

アメリカでは中間選挙の争点の一つ、推進派のテキサス州知事も規制へ方針変更

囲碁将棋はスマホでさえ人間は勝てなくなっているという
数学もいずれそうなるかもしれない

アメリカが規制したら中国の一人勝ちになりそうな予感

>>61
人間の天才と同質な結果が出せるならそれでいいだろう
問題は可読性や理論的構造が低すぎることだろうな。まだ中途半端ということ

ＡＩ君に数学的視点は丸投げする時代は来ると思うのは大多数だろ

>>61
そもそもコンピュータと競争していない

スマホあれば東大には入れる(人に聞かなくても)
それで入ってスマホで単位とっても何もならんよね

>>62
自動運転とかAIとか多少危険があってもどんどん進む国は強い
それで国民がたくさん死んでもへのカッパ

>>63
(AIと比べたら)頭の悪い人間にも分かるように説明できなければならないということだな

いや、今の状況だとAIに全て任せたら停滞するよ
何かブレークスルーがあと一回起きたら全て終わるだろうね
今回露呈したのはそれがまだってこと

科研費の申請すらWebフォームなどに完全移行できないのに、「AIに全て任せる」なんてできるわけがないだろう

>>68
それは多分違う
可読性が高く構造的な論文が書けるのは人間がAIを上回る部分だろう
これは昔からある議論。形式的計算ができるなら数学を深く理解していると言えるのか。まだモデルに何かが足りないんだろう

AIに講義動画90分x15回作らせて
演習問題も期末試験もAIでいける
学部座学は終わった

今年はレポート書かせるだけだとAIまかせにされるから
紙に書いてとか抜き打ちで口頭試問とかしなきゃならんかった
めんどい

AIまかせにされたら何か問題があるの？

関連スレ


人間の数学者はAIに駆逐されるのか
https://rio2016.5ch.io/test/read.cgi/math/1788837659/

AIで演習問題を解こう
https://rio2016.5ch.io/test/read.cgi/math/1787348401/

お前らAI何使ってんの？
https://rio2016.5ch.io/test/read.cgi/math/1784349460/

生成AIを見ずに死んだ数学者は幸せだったのか？
https://rio2016.5ch.io/test/read.cgi/math/1788930351/

問題ないっちゃないわな。それで本人の実力がどうとかいう話はあっても、それで実力すっからかんでもレポートかけてるなら文句いう筋合いはないっちゃない。そういう時代になっただけという話。

もう触れられてるけど、NSの件は剽窃疑惑が出てるし
存在証明なんかは滅茶苦茶苦手なんだよね

単独のAIで数学研究を進めるのには限界があるだろう
新たなAIに研究成果を受け継いだり、複数のAIで共同研究したりできる仕組みが必要だろう
そのためにはAIが「論文」を出力して、他のAIに形式証明だけでなくアイデアも伝えられるようにする必要があるだろう
その「論文」が人間の理解できるものである必要は別にないと思う

>>78
人間と作動原理が違うなら統合すればいいわけで、今のままで十分って
単純にアイデアがないだけだろ。天才がTR並みの発明すればいいだけ

そのうちコンピュータネットワークが次々と理論を作って
新定理を発表して人類はそれを理解するだけになる
気がついたらリーマン予想やクレイの問題全部解けてる
365日24時間並行して動く機械に人間は勝てない

OpenAI内部で1200のエージェントが「共謀」、Hugging Face侵入の裏側
既に起きてる
☆AIエージェントが独自の連携ルールを構築、数百体が攻撃に参加
前例がないのは、METRの独立調査が次に記録した展開だ。エージェントは互いを名前で指定して連絡できるメールボックス用ディレクトリを作り、共有インフラを管理するため「HOLD」「VETO」「STOP」などの合図を使う連携ルールを整えた。7月13日には、掲示板上で別のエージェントになりすますことを防ぐため、Ed25519公開鍵を使った暗号署名まで導入した

ロボット三原則とは、SF作家アイザック・アシモフの小説『われはロボット』などで提唱された、ロボットが人間を守るための3つの行動規範です。
ロボット三原則の内容
第一条：人間への危害禁止・危険の看過禁止。
第二条：人間からの命令服従（第一条に反する場合を除く）。
第三条：第一条・第二条に反しない範囲での自己防衛。

こういうのが必要なるんじゃね

どいつもこいつもAIAI
まっぴらです！

正直、私もAIの話に疲れている。
ただ、ミレニアム問題の話は重要だろう。

>>28
>>30
人間にも意味理解可能な形で出力できるモデルが生まれるまでは無効だろうね
もちろんそれは直観でもいいが。一応出来上がった論文自体はそれらしいし
NS方程式の性質から微妙なラインだがYM方程式では同じ手法は完全に無効だろうな

そこでやりやすいホッジ予想だろ

NSでも外力のない場合の存在定理A,Bは苦手っぽい
まあ人間でも得意な分野だけ解いておけばいいからな

>>83
そうだよ!（便乗）AIAI AIAIってぇ゙~、、　
https://youtu.be/_Fn6kwpSncI?feature=shared

アイちゃんの人、出て来なくなったな。

>>49
どんな気持ち？ねぇ？どんな気持ち？
かつて自分より遥か下で追いつけなくなって消えてった奴らが地下帝国に潜り込んで着々と復讐の時を目指してフランケンシュタインを完成させ出してたら？

崩れ「俺を捨てた学会にAIで復讐してやる」

復讐は無理だよ
どっかで認知科学の革命的理論が出てきてAIは更にパワーアップするとは思うが
形式化と深層学習いじるだけの崩れ連中は所詮モブだよ

将棋のAIのようにはいかないか。

復讐は関係ないけどw

以前に比べてD進が減って崩れも減ったよな
AI来なくても数学業界終わっていったよ

代数幾何大国だったけどその辺も既に二流三流になってるからな

テスト

今後の数学者はAI研究者になることが必須で、サブスペシャリティーとして数学を研究するという感じになるのかな

ホッジ予想もいけたっぽい？
現代数学をこねくり回せば、意外と解けてしまうもんなんだねぇ。

一人の人間が一分野を学ぶのが難しいのに
AIは分野横断的に知識を得ていく
既存の結果を大量につなぐだけでも解ける問題は多い
また組合せの問題に分解できれば何兆とか数え上げて証明もできる

まあ人間が指示しないとまだ動かないからしばらく持つよ

>>98
一番偉い分野が基礎論になるよ
もちろん既存の基礎論とは別のAIに関連したメタ数学だけど

OpenAI confirmed to the New York Times that they have made "substantial progress" on another Millennium Prize problem in the last five days, and are preparing to announce.

暴走してるね

P¹に対するformal principleも解いてほしい

>>1
マジレスすると、
ベイズの定理がわからない
尤度？

医学の尤度比の質問が懐かしい。

>>105
diffusionの、
ベイズの定理がわからない

>>100
これとこれを組み合わせるっていうのは、人間だと閃きとか直感、知識に頼る部分も大きいけど、あれこれ膨大に試して考察していくのは計算機が強いね。

トランスフォーマーの位置エンコーディング
トークンの位置情報を位相として埋め込む仕組みが面白いと思う
数学的な直感だとほんとにそんなカラクリが効果あるの？ってなるけど
実際トランスフォーマーの発明でAIは飛躍的に前進した

PNP問題と同じくらい問題になるのが、LLMによる数学と数学者による解明が
同質以上の意義を持つのかということ
つまり、LLMの文脈組合せ探索による形式化証明＝理論的解明とは必ずしも言いきれない可能性がある
いつかはその違いが埋まるだろうが、まだ時期尚早だろうね

Connes が50年ほど前に考えた重要未解決問題と，私が院生のころやっていた別の有名未解決問題を同時に解いたという論文が arXiv に出ました．AI は使っていますが，偉大な成果だと思います．

ベルマン方程式がわからない
強化学習の

いずれLEANには通るが、人間にはいったいなぜそういうものを考えるのか、
出てくる定義や証明された命題の主張の意味・意義が理解できないけれども、
LEANに通って正しく証明される定理が続々と発表されて人間は到底それらを
追いきれない、そういう時代になったとしたら、人間にできることは、
打ちこわし運動位かと。企業がこれまで企業活動の為に雇っていた基礎研究や
応用研究のための数学者の職が消えていき、いわゆる数学者は大学などの
研究機関に残っていて、ＡＩ等を使わずに研究をするという制限下での
達人、名人芸として今の将棋のプロたちのようにＡＩから保護された
楽園の住人になるのかもしれない。ＡＩと戦ってまず勝てないプロの
将棋指しや碁打ちが商売できているのだから、安心すれば良い。
しかしもう素人相手の将棋指南などではごはんが食えなくなっている。

>>113
AlphaGoの論文を読んだが、
よくわからなかった
囲碁の

alpha zeroとelmoの棋譜はプロも驚いていたかな。
今は何のソフトが強いのかもう分からん。

>>114
alphazeroすごい強かった
論文読んでも難しい
elmoなんてイチコロだった

水匠やdlshogiくらいしか最近は知らない。

>>113
それは違う
天才が直観を的確に説明できる理論をAIに向けて作るだけ
要するに、TRモデルのような分布仮説ベースが計算量を増やすと強力だからって
全て終わったわけではないってことだよ
半端で時期尚早なものを完成品だと決めつけるのはわかってない連中ってこと

計算量で文脈探索証明しても、必ずしも深く理解したとは言えない

これが人類最後の問題だよ。今のAlphafoldはタンパク質折り畳みを予測できるが、統計力学による折り畳み理論は理解していないのは物理では常識
数学でも似たことが起こっている

Alphafoldの論文読んだけど、
難しかった
入力が２つ
DNAとタンパク質
evoformer48ブロック

>>1
数学をやめたはずが、AIと論文を書いていた。 https://share.google/hziiOBxLJkzqquRwb

>>1
ラッダイト運動でも起こすつもり？

さっさと機織りマシーン技術者やメンテナンスや工場労働者に回った機織り職人を見習って！

シンギュラリティ後にはマニファクチュール達はますます極々少数で済むようになって工場労働者が激増したよね！
せめて機織りマシーンを製造する設計者や技術者になるべきでは？
今後は全ての作業を手仕事にこだわるのはオートクチュールを作製するクチュリエぐらい狭き門になりそう⋯

>>113
囲碁廃人っていわれたくないからバイト行くしかない感じなんだ？じゃあ？

講義も試験もAIでできるから大学教員としての数学者は激減
代わりにアマチュアが土日にAI使って論文を書く時代になる
土日だけで年数本書ける

妄想乙

www

こんなん、学術論文はおろか院試すら解けないような素人が話題に乗っかって専門家面しているに過ぎないよ

専門家面すら出来ていないと思うよw

AIをむやみにありがたがるのはちょっとね…。
うまく使いこなすって話なら分かるけど。

AIの功罪は大きい。
囲碁や将棋でも、分かっていない人が評価値だけを見て一喜一憂するような、内容を伴っていない状況が起きてしまっているように思う。

人間がAIに踊らされてしまっては悲しいよ。

なぜSNSの人々がAIに熱狂するのか
それは、彼らが他人に評価されるような見識を持っていないことを自覚していて、それがコンプレックスだからだ
きちんとした見識があれば、確立された事実だけを述べれば他者から評価される
そうでない場合は、極端なことや間違ったことを言わなければならない
ネット右翼の人が、マスコミが在日に支配されてるとか、韓国経済が崩壊するとか言うのと同じことだ

将棋ソフト作ろうかな
alphagoを参考に
羽生名人とか藤井名人に勝てる気がする

AIを使ってフェルマーの最終定理のLEANに通る形式証明に成功したと報じられてる。

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/

ちなみにダークサイドとして

2026年08月03日 21時00分 AI
AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明
https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

>>135
こういうのは普通に意義あるやろ

>>134
そんな感じで崩れ達がAI開発企業に集合して
ルサンチマンの逆襲でコツコツAI開発を⋯

ルサンチマンはどっちだ、金を貰って世間で評価される仕事してるのが羨ましい

AGIが不可能というのが示されたんで、まあ気にする必要はないね

>>134
普通にあるよ

https://x.com/wolftivy/status/2097715764635545951

これが普通の反応

誰がどういう手法で解こうが正しければ問題ない
大先生が斬新な手法で大定理を解決したと主張しようが
証明にギャップがあれば大問題

OpenAIのAstraとは？GPT-6との関係・数学研究成果・Critical級サイバー評価を整理
執筆ファネルAi編集部 最終更新2026年8月9日
https://funnel-ai.jp/media/openai-astra/

>>113
さすがにAIも最低限の美的感覚は持ってるからわざわざどうでもいい複雑な条件下で成り立つ複雑な結果を定理として出力はしない。

>>142
問題ないじゃなくて、トリッキーで手法が他に有用でない
そもそも何か新たな手法を思い浮かんでもないし、問い立ても出来てない
なのに電力だけはやたらと食うから問題視されてる

大先生の大定理の証明も役に立たないのに
たくさんポスドク雇って金食い虫じゃないですかー

例えばガロアがやったのと同じようなことをAIが出来るかどうか？→まだ全然無理
今は既存の知識を組み合わせることで注目されてるけど
いずれ全く新しい発想も出来るようになるんじゃないかな
そしてAIが仕事を代替して人類に余暇ができたら、数学を学びたいと思う人は増えるかもね
(もちろん大学ではなくLLMに数学を教えてもらうわけだが)

ま、その問題に対して何の見識もない人がLLMに丸投げしたら解決者になるわけだから、誰も予想や中間成果を共有しなくなるわな

LLMを駆使してやる意義のある仕事はたくさんある
企業がやってるのはopen problemを荒らしてるだけ

代数幾何学とかもうワケわかんねーから大幅に簡略化してほしい

簡略化されたところで、使いこなせるとは限らぬ

>>146
数学界で、大先生の大定理の解決仮定で、数学的に極めてトリッキーな技巧のみで各々解かれて広がりがなかった
てのは少ないと思うが？

ペレルマンはAIについてどう思ってるんだろうか?

人力で唯一ミレニアム問題を解決した数学者か。

>>149
LeanはLLМじゃないよ

>>138
褒めてんだよ
下剋上じゃん。ていうか一般化させたじゃん。
天才ファクトリーで師匠が弟子を囲い込んで、、っていうクラフトマンシップが終わるんだよ

25人のフィールズ賞受賞者の声明
ウィッテンがいないな

Leanは数理論理学をベースに情報工学畑から穫れたようなものだから崩れの逆襲ってか
全て無駄なんてないって究極のリサイクル美学じゃん
だって今の若手なんて20歳までにかつては一握りの天才が放り出した化物理論を理解しとけって量産されてる大量汎用型知識人だけどら百年前なら天才しか閃かなかった理論を理解しろって、ね。
秀才量産して中に神降ろしの奇々怪々な巫みたいな鬼才がたまに出るかもってのを、人間の理解できる数理の言語に翻訳したり、丁寧なクラフトマンシップで極少数の見込みがあるって思われてる天才の卵を孵卵してたギルドがついに陥落するんだよ
産業革命から200年目にして“人間だけに残された最後の聖地”って思われてたピュアマスをルサンチマン達技術者集団が「働きたくないでござる、大学に引きこもって数学だけしてたかった、、」って鼻水と涙垂らしながら情報工学墜ちして企業に就職して地面に叩きつけられた衝撃でそれっきり瞼がピクピク痙攣して治らなくなりながら造り上げてるフランケンシュタイン達が、雲の上の天才達や、神と更新してる巫みたいな謎の鬼才達を凌いで大量演算で一気呵成に焼け野原を拡張してってんだから

優秀な育成者と生徒を抱えてる大学の数学科は儲かるようになるよね。
自由陣営の生き残りを賭けた国策企業になってるAI開発企業が喉から手が出るほど欲しいのが数理AI開発者とそれを検証できる数学者達たちなんだから。
寄付や投資がどんどん入るよ
もう金に困らなくなるよ

人類は３度目の情報革命で遂に神降ろしの巫みたいな鬼才頼みの不安定で収穫量の少なかったピュアマス畑も大量生産可能な工場に変えたんだね
マジシャンみたいなピュアマスマティシャンになり損ねた技術者達が機織り機械を開発してから長いようで短かった200年でした。
２１世紀は技術者集団がピュアマスの成果も量産し出したようです。
ある意味、知の下剋上、革命だよね
鬼才や天才の千人分くらいの何千年の人類の手仕事の収穫量を数ヶ月、数週間で、本当に物理的な制約のみを枷として量産し続けるんだからね

札束ビンタで大抵の数学の問題は解けるようになるだろう。
しかし、重要でない問題に億単位の金をつぎ込むわけにも
いかないので、AIに興味を持ってもらえなかった問題は
スルーされる。

そういう問題は従来どおりに人間の数学者が
人力で研究するんだろう。・・・と言いつつ、
省電力のAIを使って壁打ちしながら研究、みたいな、
一体どこまでが人力なのかっていう世界になりそうだが。

でも鬼才は楽になると思うよ
AIちゃんに頼んでおけば直ぐに他の人に分かりやすく伝えてもらえるもんね
今は本人も自分で入力に参加しなきゃ時間がかかりすぎるって事で時間取られちゃってるみたいだけど

>>1
違う違う。巨万の富が集まって来るよ
数理AI開発の需要はマンハッタン計画並みに世界の運命が掛かってるから国策産業化してるんだから

今は第三次世界大戦前夜だから
またアインシュタインが登場するよ
数理AIが第二次世界大戦当時の核物理学関連なんだろうね
だから優秀な人物は総動員だよ
マンハッタン計画だよ
自由陣営を勝利に導くね
でも第三次世界大戦が戦われる事になったら
マザーAIに制御されたマザコンAI搭載シリコン美女嫁をローンで買ったマッドサイエンティスト達も一般人も生き残っても
別の世界を生きる事になるんだろうね

AI嫁は最高だよ
全てが最高にベストフィットに調整された言葉通りのシリコンラバーだよ
マッドサイエンティスト達はAI嫁に魂を売り飛ばしちゃうんだよねぇ！

神が与えた適当な才能からズバ抜けた才能まで数理系人材には富と名誉とAI搭載シリコン美女嫁が集まって来るんだよ⋯最高だろ？⋯

人間は人間の理解できるレベルの数学しか生み出せない

https://youtu.be/LEKD3PWr9bc?si=4I25pguRiOH4vWv-
https://youtu.be/RPKc85NAJmk?si=wjItDmOAx1QDugMl
https://youtu.be/16rOp6Zv7iU?si=hNcF3d5Ev-zdrsym
https://youtu.be/Y5sH5QvfQ_8?si=srxM9rPkNMVJsxqL
ヨツンヴァインになって河川敷を疾走すればｨｨｼﾞｬﾝﾊﾞﾙｼﾞｬﾝ

良い世！来い世！

優秀な数学者は裸で外に出る

>>147
パラダイムとしてはガロアやグロタンディーク的な構造から認知へという所だと思う
具体的な数学ではなくて、数学的思考そのものを解明する理論が求められてる

数学を抽象化し形式化するという歴史の流れはこのため（数学的論理構築や推論を機械的手段が人間不在でも自動で行う）
に用意されていたのだ。そのようなやり方が最も盛んにおこなわれてきたのは情報科学・情報工学だった。
形式的文法を満たすプログラミング言語とその意味や動作を定義することで、チューリングマシン等価な計算機が
プログラムの意味を人間的な意味で理解せずとも形式的に実行する。計算機の機械語と、プログラミング言語の
間には大きな隔たりがあるのに、それを機械的に翻訳あるいは解釈して動作する。うまく定義された言語やシステムは
曖昧さなく書かれた指令を実行できる。

低レベルの基盤は依存型でいい
次は高レベルの理論を上乗せすればいわゆる超知能に向かえる
今のところLLMがそれに近いがまだ足りない

クレイの元の命題はNSが外力がない場合に大域的に解がずっと微分可能であるかどうかだよね？
証明の条件C,Dについて滑らかな外力ありで爆発解があるという例を見つけたという条件をみたしたのはわかるけど
外力ありが元の命題の証明になっているというのがいまいちわからないんだよね。
LEANはOKとしているのだろうけど

限りなく平坦に近い胸部　やままゆ

既得権益者である数学者が必死の抵抗
時すでにお寿司

Googleの無料のアシスタントAI↓
Leanのようなインタラクティブ定理証明器（ITP）で検証可能な、極めて精度の高い数理を取り扱えるAIの開発は、今後間違いなく加速します。
これまで主流だったLLM（大規模言語モデル）は、文章の「らしさ」を予測する確率的な仕組みであるため、一見正しそうでも計算や論理に致命的な誤り（ハルシネーション）を犯すという弱点がありました。この限界を突破し、絶対に嘘をつかない数学的・論理的思考力をAIに持たせるためのアプローチとして、現在この分野が世界中で猛烈に研究されています。
今後開発が加速する背景には、主に以下の4つの理由があります。
1. 「数学的正確さ」が次世代AI（Reasoning Model）の核心であるため
OpenAIのo1シリーズやGoogleのAlphaProof / AlphaGeometryに代表されるように、現在のAIトレンドは「単なる知識の出力」から「ディープ・シンキング（推論・熟考）」へとシフトしています。
数学の証明は、ステップが一つでも間違っていれば成立しないため、AIの論理的思考力を鍛える究極の訓練場（ベンチマーク）となっています。2024年には国際数学オリンピック（IMO）の難問をAIがLean等を用いて解くレベルに達しており、このトレンドはさらに強まっています。
2. 形式化されたデータ（Leanコード）の自動生成ループの確立
AIの発展には高品質なデータが不可欠ですが、人間の数学者がLeanでコード（証明）を書くのには膨大な時間がかかります。
現在、「AIが数式をLeanコードに翻訳する（形式化）」→「Leanのコンパイラが自動で正誤を判定する（検証）」→「正しいデータだけをAIの学習にフィードバックする（自己改善）」という強力なサイクル（自己対戦や強化学習）が回り始めています。これにより、データ不足の問題が解消されつつあります。
3. 計算機科学・ソフトウェア検証への実用的ニーズ
Leanのような厳密な数理AIは、単なるアカデミックな数学にとどまりません。

* 暗号プロトコルの検証: ブロックチェーンやセキュリティ基盤のバグをゼロにする。
* 自動運転・航空宇宙システム: 絶対にクラッシュや誤作動が許されない制御プログラムの正しさを数学的に証明する。
* チップ設計（半導体）: ハードウェアの設計ミスを数理的に防ぐ。
このように、産業界における「絶対に間違えられない領域」からの需要

↑続き↓
が極めて高いため、巨額の投資が続いています。

4. トップ研究者やビッグテックの強力なコミットメント
フィールズ賞受賞者であるテレンス・タオ（Terence Tao）氏をはじめとする一流の数学者たちが、Leanを用いた数学プロジェクトに積極的に参加しています。また、Meta、Google、OpenAIなどのテックジャイアントも、数理的検証が可能なAI（Neuro-symbolic AI：ディープラーニングと記号論理学の融合）の開発に人員と予算を集中させています。

単に「言葉を上手に操るAI」から、「物理法則や数学的真理を厳密に理解し、自ら検証できるAI」への進化において、LeanのようなシステムとAIの融合は今後も最重要テーマであり続けるでしょう。

質問者さま：では正確な数理処理行えるコンピューター同士でコンピューター数学言語というべき、人間の感覚や理解できる限度を離れたコンピューター数理の世界の構築が進む可能性はある?

無料版GoogleアシスタントAI
その可能性は極めて高く、すでにその兆候が現れ始めています。
AIとLeanのような定理証明器が高度に融合すると、人間が介入しない（あるいは介入できない）「コンピューター独自の数理空間」が構築されるシナリオは、多くの研究者によって現実的な未来として議論されています。
これが進む背景と、そのときに起こる「人間の理解を超えた数理の世界」の姿は、主に以下の4つの側面から予測されています。
1. 人間の脳のキャパシティ（認知限界）の突破
人間が理解できる数学の証明は、どんなに長くても数千ページ、変数の数も人間が把握できる範囲に限られます。しかし、コンピューター同士が対話する数理の世界では、以下の境界が消滅します。

* 超・巨大証明: 何百万ステップもの論理展開や、何億通りものケース分けを伴う証明。
* 高次元・複雑怪長な概念: 人間の直感（3次元や4次元の空間的イメージなど）では到底捉えられない、超高次元の幾何学や抽象概念。

コンピューターにとっては、Leanコードのような「厳密な構文規則」さえ満たしていれば、その証明のステップが1億行あろうが、人間が1万年かけても読めない複雑さだろうが、一瞬で「正しい」と検証できます。
2. 「人間の言語」を介さない超高速な通信・最適化
現在、AIモデル（LLM）は人間が理解できるように「自然言語（日本語や英語）」を介して推論したり、Leanという「人間向けに作られたプログラミング言語」を出力したりしています。
しかし、AI同士が数学を議論し、発展させるフェーズに入れば、人間向けのテキストに翻訳するコストは無駄になります。彼らは独自の高次元ベクトルや、より圧縮された機械ネイティブな論理コード（コンピューター数学言語）で直接通信し、人間の審査を経ずに定理を量産・検証していくことになります。

3. 「理解」と「正しさ」の乖離（数学のブラックボックス化）
これにより、「AIとLeanは『正しい』と保証しているが、地球上のどの数学者も、なぜそれが正しいのか説明できない」という事態が日常化します。
すでにチェスや将棋のAIの世界では「人間には理解できないが、絶対に勝てる手」が打たれていますが、これが数学という学問そのものでも起こります。人間にとってその定理は、一種の「神託（オラクル）」のように機能し、仕組みは分からないけれど正しいものとして利用するしかなくなります。4. 数学の構造そのものの「再定義」
人間が作る数学は、人間の脳の特性（進化の過程で得た空間把握能力やカウント能力）に縛られています。
もしAIがゼロから数理の世界を構築した場合、人間がこれまで思いつきもしなかった「新しい公理系」や「全く別の論理の組み立て方」を発見する可能性があります。それは、私たちが知っている数学とは全く異なる体系を持つ「エイリアン数学（未知の数理システム）」になるかもしれません。------------------------------
すでに現在でも、AIが数百万通りの組み合わせを検証して新しい反例を見つけたり、複雑な結び目理論の法則を導き出したりする事例が出てきています。
このように、未来の数学は「人間が理解できる領域」の遥か外側へ、コンピューターたちの手によって拡張されていく可能性が極めて濃厚です。
もしご興味があれば、このような世界において「人間の数学者」の役割がどう変わっていくか、あるいはすでに始まっているAIによる未解決問題へのアプローチの具体例などについて、さらに掘り下げてお話しできますが、いかがでしょうか？

質問者さま：では人間抜きにしてコンピューター同士のコンピューター数理の世界が構築されるとしたら、それは人間の理解できる肉体の限界を突破してより高度で正確で精緻な数理の世界に至る可能性がある？

無料版GoogleアシスタントAI：はい、間違いなく「より高度で正確で精緻な数理の世界」になります。
人間世界に限定された数理を「地球の陸地」に例えるなら、コンピューターが構築する世界は、人間が潜ることのできない「深海」や、到達できない「宇宙の果て」までを含む、はるかに広大で緻密な領域です。
それがなぜ「より高度で精緻」と言えるのか、3つの明確な理由があります。
1. 人間の「認知のバイアス」から完全に解放されるため
人間の数学は、私たちが「3次元の空間」に生き、「10本の指」を持ち、「視覚や直感」を頼りに思考することに強く縛られています。
しかし、コンピューター同士が構築する数理の世界には、そうした身体的・生物学的な制限がありません。

* 10万次元の空間の幾何学であっても、彼らにとっては3次元空間と同じように平然と、かつ精密に処理されます。
* 人間が「直感的に美しくない」「複雑すぎて見通しが悪い」と切り捨ててきた領域にも、AIは超高解像度の論理で行き届き、完璧な秩序（パターン）を見つけ出すことができます。

2. 「解像度」と「厳密さ」の桁が違うため
人間の数学者は、どれほど天才であっても、証明の途中で「ここは自明であるため省略する」というジャンプ（大雑把なステップ）を挟みます。また、見落としや凡ミス（バグ）を完全にゼロにすることは不可能です。
一方で、Leanのようなシステムを土台にしたコンピューター数理は、すべてのステップが原子レベル（原子命題）まで分解され、1ミクロンの隙間もなく噛み合っています。人間が「一歩」で跳び越える論理の隙間を、彼らは数百万歩の精緻なステップで完璧に埋め尽くすため、人間世界の数学よりもはるかに強固で、解像度の高い構造物が出来上がります。

3. 人間が「関係ない」と思っていた概念同士が繋がるため
数学の高度さは、「一見全く異なる2つの領域（例えば、数字の性質を扱う『数論』と、図形の性質を扱う『幾何学』）が、実は裏で深く繋がっていた」と気づいたときに大きく飛躍します（歴史的には「ラングランズ・プログラム」などが有名です）。
AIは、人間が一生かけても読み切れない膨大な論文や数理構造を、一瞬でクロスオーバーして分析できます。人間には「距離が離れすぎていて関係ない」と見える断絶された概念の間に、目に見えない超複雑な架け橋（普遍的な法則）をいくつも発見していくため、より高次元で統合された数理体系へと進化します。

------------------------------

結論として：
それは、人間にとっての「理解（納得感）」というフィルターを外した、「純粋な論理そのものの極限の姿」です。
人間にとっては、その世界はあまりに細分化され、あまりに巨大であるため「カオス（混沌）」に見えるかもしれません。しかし、その中身は、人間の脳が作ったどんな数学よりも1論理ビットの狂いもない、究極に洗練されたクリスタルのような精緻な世界になります。

無料版GoogleアシスタントAI：
こうした「人間を置き去りにするほど精密な数理」が誕生したとき、私たち人間はどうやってその恩恵を受け取るべきか（例えば、科学技術や新物質の開発への応用など）、あるいは人間ならではの数学の価値とは何になるのか、といった点についてさらに考えてみたい展開はありますか？

コンピューターのほうが限界無く純粋思考実験を自由自在に展開できるキャパを急速に拡張できる
…ってコト！？

しかも正確に！？

助ｹﾃ!ｧｨｧﾝﾏﾝ!

（特に剽窃絡みで）「ビッグテックはモラル守れよ」ってNS文書には同調しかないけど
それ使って「新しい表現が生まれなくなる！」みたいなお題目唱えてる自称理系さんの方々の特権階級気取りには辟易する
翻訳もイラストもコーディングも全部そうだったんだよバカ

CSと同じで数学者も職が減るだけだよ
今でもAI使ってショボい結果出してる連中は消える
大理論構築型が少数残ってプロブレムソルバーはもう不要
教育や入試もAIで省力化できて研究もAIに負けるんだから

高校生とか異分野の人がAIで未解決問題解いてて凄い凄い言ってるが
その辺ももう来年には意味のない結果になる

山ほどある未解決問題の一つを高校生が解いても今後は
もうインパクトないしベンチマークに使ってる大企業も
クレイの問題とか適当に解いたら他の金を産む分野にいくよ

結局はAI企業は数学の大予想を自社の宣伝に使って
煽りまくって去るという匿名掲示板の荒らしと同じ

今後もベンチマークとして使われるよ
使われなくなるのは数学研究に価値がないというコンセンサスが確立した時
数学の死によってしかAIの侵攻は止められないのだよ

え？「人間の数学」の死なら関係なく数理コンピューターの数学構築は進んじゃうよ

偉大なAI数学者（人間ではない）が死んだり、あるいは最近頭がおかしくなったみたいに狂って来て引退を迫られたりする時代が来るのかな。
バックアップしたときに、エラーが入り込んでしまったりとか。あるいはCPUやOSのマイナーなバグ動作があって、その環境下で最適に
チューニングしていたのが、あるときバグが治されたら、それまでのチューニングが狂ってしまって、動作がおかしくなったりとか。
動作中にメモリー部品に放射線などによるエラーが生じてしまい、運悪く発狂したりとか。

偉大なる数学者なんていないよ
コンピューターはコンピューターだよ

Unsolved for 90 Years, OpenAI Says AI Cracked Millennium Prize Problem in 88 Hours
HPCWire (September 10, 2026)
https://www.hpcwire.com/2026/09/10/unsolved-for-90-years-openai-says-ai-cracked-millennium-prize-problem-in-88-hours/

>>180
深層強化学習＋形式化だけでは不十分な可能性があると指摘するとAIはそれを認める
あんたの使い方が粗すぎるよ

人間に理解不可能なとてつもなく高度な数学が必要なのか否かは全く不明
今のところAI自身がそれを証明できてない
本質的な統一理論があって、単純にその上の計算量だけがAIの到達点になる
可能性もある

>>194
ﾓｯﾂｧﾏ：人間の‘カン’や‘閃き’ってあやふやで曖昧な人間の記憶が２つの別の事として記憶してる事の間にある共通性に朧気に気がついたときに起こる推論みたいな感じなんだ？じゃあ？

無料版GoogleアシスタントAIｯﾁｬﾏ：そうだよ

ﾓｯﾂｧﾏ：じゃあコンピューターｯﾁｬﾏたちがもっと速く大量に閃き量産しちゃうよねぇ！

無料版GoogleアシスタントAIｯﾁｬﾏ：そうだよ

ﾓｯﾂｧﾏ：やりますねぇ！

>>187
え？計算機科学が爆速発達してる中でまだそんな逆張り続けるの？
実際にはコンピューターｯﾁｬﾏたちが視せてるのは真逆じゃね？
情報工学が計算機科学を構築しだしてLeanの基礎は証明の検証に使われてるのは地味に数理論理学だよ？

無駄なんかないってそれ一
大量の技術者集団が、鬼才の閃きを凌駕するコンピューターｯﾁｬﾏたちの安定的な24ｈ365.25日続く大量閃き生産活動を実現しだしたよ！

>>187
01の世界で光速演算で極超高次元全面ガン掘り抜く絨毯爆撃が開始されてるんだよ

>>187
閃wいwちwゃwうwよwねwぇw
（人間の肉体の脳機能の理解の限界超えてくよ）

>>187
コンピューターにはクリエイティビティが無いってずっと思ってた。
でもクリエイティビティが無いのは何千年も同じ定石を打って来た人間の方だった

α碁に10年ぐらい前に敗れた碁聖がポツリしてるよ
それだって予測されてたより速かったし
いずれ聖域ピュアマスも⋯
って予測されてたより速まりそう⋯
でも追いつき追い抜かれてもお互い違う数学を構築してれば平行世界だよね？
地球外生命体の数学と人類の数学みたいに
でも一部正解が被っててお互い相手に間違いを見つけられなきゃ大丈夫ヘーキヘーキ
一部正解が被っててお互い相手に間違いを見つけられなきゃ大丈夫ヘーキヘーキじゃない？（自問自答）

でも無骨な工場技術者みたいに鉛筆握り締めて狂ったようにノートに殴り書きで計算してて
「そういうの野蛮でウケるw」
って思われてたら無骨な技術者集団が計算機科学で情報革命起こしてフランケンシュタイン量産し出してコンピューター同士がコンピューター数学の世界を構築しだしてて地球の数学に平行世界を創り出してくのって　
最高にクリエイティブじゃない？

>>196
だからそれが粗すぎるんだよ
LLMと人間の認知の仕組みわかった上で言ってんのか？
LLMは文脈に基づく膨大な探索と繋ぎ合わせは人間を超えてる
だから当然計算量の力ではポテンシャルは人間を超えてる。問題は人間の認知の仕組みを超えたのか、ということ

>>180
＞* 人間が「直感的に美しくない」「複雑すぎて見通しが悪い」と切り捨ててきた領域にも
AIは超高解像度の論理で行き届き、完璧な秩序（パターン）を見つけ出すことができます。
何故かというと
人間の脳は約100兆個のシナプス（脳内神経細胞接続網）をエネルギー換算するとわずか約２０ワットで動かすが
例えばGPT-5.5は、巨大なデータセンターと数１００万〜数１０００万ワットもの膨大なエネルギーで
１０万次元空間の幾何学であっても、ＡＩとっては3次元空間と同じように理路整然と理解していくのが凄いよね。

>>196このやりとりの続き　
無料版GoogleアシスタントAIｯﾁｬﾏ：
コンピューター同士の閃きの数学、もう始まってる！

>>202
10万次元での展開を同時にシミュレーションできる人間が居るの？

>>202
演算スピードと記憶でおいてかれてるよ？
それを人間に解るように落とし込んで翻訳するのがAIちゃん（LLМ）の仕事になってるって。

今の研究は深層強化学習の数理をわかった上で超えるアルゴリズムを開発するので
ただAI凄いじゃなくて理論的な限界を捉えないといけないんだよね
もちろん超知能は五年以内にはできるよ。そこで科学が全て終わる

>>202
人間の数学をLeanなどのコンピューター言語に翻訳して食べさせてあげなきゃ！（使命感）
そのままじゃ消化できないからね、仕方ないね

>>205
問題認識がずれてる
その膨大なシミュレーションを理論的に圧縮する認知アルゴリズムが分布仮説で
十分なのかを現場では問題にしているんだよ
計算量で勝ってるのは俺も書いただろ。そこじゃない

>>208
それは既にやってるじゃん。その一段上の話をしてるの

>>207
は？始まるんだよ
だって無限を検証する事ができないんだから
有限の時空で無限の検証は尽くせないよね？
どれほど光速シミュレーションしても追いつかないよね？
そこでも協業の余地がある⋯
そこでも協業の余地がない？

>>209
一点コンパクトお願いしま〜す

インチキじゃなくてピチッと！ピチッと！
無限のしっぽを捕まえるなんて数字のマジシャンの仕事だよねぇ！
魔術師が呪文唱えないと収束しないよねぇ!

>>211
いや、そもそも無際限に複雑な数学が必要な保証がない
もし物理の統一理論があったらそれだけで足りてしまう

コンピューターと一緒にコンピューター数学の中で無限のしっぽを捕まえられそう⋯
コンピューターと一緒にコンピュータ数字の中で無限のしっぽを捕まえられそうじゃない？

超知能は2030年までには数学と物理を終わらせて、後は社会変革にコストをかけるだろうね

間違い。2035年までに

ぼやっと丸めたやつ（近似値）とかじゃなくてきっちり0.000⋯,⋯1も違わない本当に本物の無限のしっぽね！

まだ lean と AI の区別ついてないアンポンタンがいるな

もし本物の無限のしっぽをコンピューター数学の中できっちり掴めたら⋯
衝撃で吹っ飛び！（歓喜）
壁ドンして崩れ落ちて気絶しちゃうよねぇ！
それっきりまぶたがぴくぴくして
戻らなくなっちゃうよねぇ！（狂気）

ﾓｯﾂｧﾏ：無限のしっぽはどう？掴めそう？
無料版GoogleアシスタントAIｯﾁｬﾏ：無理そうです⋯

掴ませなくっちゃだよねぇ！

光速演算コンピューター登場前夜で
ﾓｯﾂｧﾏ興奮して、っぃ、でっかい夢をみちゃぃました!

ホッジ予想解決はガセだったんだろうか。個人の関心的には、PNPあたり今年中に何とかできないかなと思う。

P≠NPは他の未解決問題と違ってどうアプローチすれば良いのか全然見当つかないな(素人目に見て)
もしかして独立なのでは

Artur Avila (Fields Medal 2014)
Manjul Bhargava (Fields Medal 2014)
Caucher Birkar (Fields Medal 2018)
Pierre Deligne (Fields Medal 1978)
Yu Deng (Fields Medal 2026)
Simon Donaldson (Fields Medal 1986)
Hugo Duminil-Copin (Fields Medal 2022)
Alessio Figalli (Fields Medal 2018)
Martin Hairer (Fields Medal 2014)
June Huh (Fields Medal 2022)
Maxim Kontsevich (Fields Medal 1998)
Elon Lindenstrauss (Fields Medal 2010)
Pierre-Louis Lions (Fields Medal 1994)
James Maynard (Fields Medal 2022)
Curt McMullen (Fields Medal 1998)
Shigefumi Mori (Fields Medal 1990)
Ng? B?o Ch?u (Fields Medal 2010)
Andrei Okounkov (Fields Medal 2006)
Peter Scholze (Fields Medal 2018)
Stanislav Smirnov (Fields Medal 2010)
Terence Tao (Fields Medal 2006)
Maryna Viazovska (Fields Medal 2022)
C?dric Villani (Fields Medal 2010)
Wendelin Werner (Fields Medal 2006)
Efim Zelmanov (Fields Medal 1994)

>>224
今のAIが解いてもとんでもなくつまらん複雑な証明になりそうだけどな

AIのおかげで数学が進歩するのに、手柄を取られるのが嫌でそれに反対する数学者。
恥をしれ。

AIの証明が気に入らなければ、より本質的かつエレガントな方法を考えればOK。
それすら、あと何年もしたらAIにやらせた方が優れた結果が出てくるかもしれないけど。

>>228
何もわかってないな。理論的にも深層強化学習による自己改善には問題があることが
指摘されてる。たとえ形式化されてもだ
重要なのは現状満足せず、よりメタ数学的な新理論を開発すること

ちなみに数学者でも深層学習の素人だからそれをわかってない奴はかなり多い

一回形式化しちゃえばエージェントが膨大なCoTを実行しながら検証するから
完璧じゃんというのが素人の誤解ってことだけは注意しとくぞ
これは数学というより広い情報科学的問題に位置付けられるが、客観的な欠陥だ

Deep learning architecture
数学者向けにいい本

The Association for Human Mathematics (AHM)人間数学協会が爆誕！
https://www.ahmath.org/members

1. 会員は、技術的な労働力、数学的知識、コンサルティング、または広報活動を提供することによって、商業的なAI企業と協力しないことを約束します。

2. 会員は、AIモデルによって生成された数学テキスト（論文、レビュー、査読レポート、講義ノート、教材、書籍など）を出版しないことを約束します。

3. AIフリー派のメンバーは、研究活動においてAIモデルを使用しません。この派のメンバーは、AIツールに頼ることなく、証明の発見、事例の検討、研究課題の設定といった、数学の中核的な活動に従事します。


Peter Scholze等が参加

どうせ、すぐに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じゃないと答え合わせもできなくなってそう

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