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同士が数学を議論し、発展させるフェーズに入れば、人間向けのテキストに翻訳するコストは無駄になります。彼らは独自の高次元ベクトルや、より圧縮された機械ネイティブな論理コード（コンピューター数学言語）で直接通信し、人間の審査を経ずに定理を量産・検証していくことになります。