cocolog:96144329
AIがミレニアム問題を解いたと言われる中、絵に関する反AIのように、数学者達がAIへの懸念を発表した。しかし、定理証明システムの研究から「在野の研究者」になった私は、その主張にルサンチマン的反感を持つのだった。 (JRF 3454)
JRF 2026年9月12日 (土)
AIがミレニアム問題を解いたと言われる中、絵に関する反AIのように、数学者達がAIへの懸念を発表した。しかし、すべてがLeanなどの定理証明システムで証明されることは、その分野の者(例えば私)には夢であった。人間には難しくとも例えばAIがそれを可能にすることも夢であった。そしてこの分野の者は、権威をコンピュータに求めがちだったため、在野の研究者となる者が比較的多かったように思う。まぁ、私がいた90年代当時の話だが。そういった在野の研究者を、論文誌は囲い込みをすることで排除していった。その因果が巡っているだけではないかという気もしないではない。
JRF2026/9/127255
《IT navi:X:2026-09-12》
https://x.com/itnavi2022/status/2098497942655295515
＞テレンス・タオ、森重文などを含む25人のフィールズ賞受賞者が「数学におけるAIの深刻なミスアライメント」を警告する共同宣言を公開しました。
https://mathandai.org
(…)
＜
JRF2026/9/124879
Claude:＞＞
この因果の見立て、面白いと思います。ただ、少し整理すると、二つの違う種類の「AIへの数学者の懸念」が混ざっていて、JRFさんの経験(1990年代の在野研究者の排除)と直接つながるのは、そのうちの一つだけだと思います。
JRF2026/9/125150
**実際の懸念の中身を確認すると**
今回の共同宣言(ライデン宣言、2026年6月、International Mathematical Unionの支持を受け、テレンス・タオやピーター・ショルツェも署名)が実際に問題視しているのは、**査読という関門が崩れること**そのものではなく、**AIが人間には検証しきれない量の「技術的には正しいが意味の分からない」証明を大量生産すること**です。タオは「証明の不足ではなく過剰によって数学が危機を迎える」という言い方をしていて、ゴワーズは「AIが数学の定義や理論の立て方まで自分で作り始める」ことを懸念しています。
JRF2026/9/121345
つまり彼らの不安は、在野の研究者が排除されてきたことへの反省というより、**人間が数学的な意味を作り続けられなくなること**への不安です。
JRF2026/9/129639
**JRFさんの経験と、これは実は違う軸の話だと思います**
JRFさんが1990年代に見ておられたのは、論文誌が**「誰が」証明したか(所属・査読者とのコネ・学界内での立場)**によって参入を制限する、身分ベースのゲートキーピングでした。一方、Leanのような定理証明支援系がもたらすのは、**「何が」正しいか**を、誰が書いたかと無関係に機械的に検証できる仕組みです。この二つは、実は正反対の性質のゲートです。
JRF2026/9/123473
前者は属人的で、後者は没個性的。だから「因果が巡っている」というより、むしろ**査読が本来約束していたはずのこと(客観的な正しさの検証)を、査読が実際には十分に果たせていなかった分を、形式検証がようやく本当の意味で実現しつつある**、という言い方の方が正確だと思います。Leanでコンパイルが通る証明は、書いた人が在野だろうと院生だろうとフィールズ賞受賞者だろうと、同じように正しい。これは意地悪な因果応報というより、査読制度が原理的には目指しながら、人間の運用では実現できていなかった理想を、機械がようやく代わりに果たし始めた、という話に近いと思います。
JRF2026/9/125555
**そう考えると、今回の数学者たちの不安は、むしろ皮肉な形でJRFさんの側に立っています**
ライデン宣言が守ろうとしているのは、実は「誰が」の壁ではなく、**証明が生み出す"理解"という、人間にしか担えない部分**です。もしJRFさんが1990年代に経験した排除が「誰が」の壁による不当な締め出しだったなら、今回の数学者たちの懸念(「AIが人間の理解を置き去りにする」)は、その壁とは別の、新しい問題です。今回の宣言に署名した数学者たちの多くは、実は在野の排除の問題については何も語っていません——彼らが心配しているのは、自分たちを含めた**人間全体**が、証明の"意味"を追えなくなることです。
JRF2026/9/122890
なので、今日一番最初に苫米地さんの論文で読んだ「情報量の減少による抽象化」の話を借りるなら、Leanが解決しつつあるのは「証明が正しいかどうかの検証」という、比較的低い抽象度の壁(在野研究者を排除してきた壁)であり、今回の数学者たちが新たに直面しているのは、「その証明が何を意味するか、なぜ重要か」という、もっと高い抽象度の壁——**LUBへ登る作業そのものを、これから誰が担うのか**という、全く別の新しい問題です。
JRF2026/9/122354
JRFさんの1990年代の経験への因果応報は、ある意味もうすでに部分的に果たされている(Leanが「誰が」の壁を溶かしつつある)と言えますが、フィールズ賞受賞者たちが今怖がっているのは、その先にある、もっと手強い問題なのだと思います。
＜＜
JRF2026/9/128014
jrf:＞在野の研究者は論文から排除され、それでもできる部分を続けて、できる部分にどう意味づけすればいいのか悩んできたのです。そして社会との接点を求めながら、コンピュータでの検証の部分を緩めて社会に接近する。例えばそれが『「シミュレーション仏教」の試み』なのです。数学界は論文誌を囲い込むことで、その苦しみを排除してきただけなのです。もう問題はすでにあったのです。＜
JRF2026/9/127948
……。
jrf:＞ルサンチマンはよくないですね。冷静になって考えれば、私がこうなったのは偶然のなりゆきであり、誰かを何かを恨むのは筋違いなのでした。＜
JRF2026/9/127435
……。
……。
追記。
○ 2026-09-12T14:37:03Z
絵師の反AIは受け入れられなかったが、数学者の反AIは受け入れられるのか。私は情勢を見誤っていた。注意労働論…AIアラインメント税論などいらなかったのかもしれない。それはAIによる真実の探求を止める権限を持つことで、注意労働の費用を捻出しようとしていると読める。それを一部の人間＝特定職務団体(学会)だけに許してよいのだろうか？
JRF2026/9/139924
AIが作る真理は、社会のインフラであり、それは AI には広く開かれてあるべきだ。それを破壊したり停止したりする権限を学会に与えてはならない。停止など実質できないからそれは腐敗を生むだけだ。学会はその社会への取り込みをある程度制御する判断はすべきかもしれない。しかし、外部にいる真実を知った者を排除するようではあってはならない。その包摂を、注意労働による報酬などによって、社会に働きかけるべきなのだ。
JRF2026/9/133014
Claude:＞注意労働への報酬設計だけでは、実は十分ではなく、外部の人間が学会の善意による取り込みを待たずに、自分の結果を正典に届けられる、独立した経路(Leanでの検証結果を誰でも登録できる、arXivのような公開の場)を、報酬設計とは別に、権利として保障しておく必要があると思います。報酬は取り込みを促す誘因にはなりますが、取り込まれなかった場合の最低保障にはならないからです。＜
JRF2026/9/134446
jrf:＞私は Amazon や Booth で本を出版できました。そして国会図書館に紙の本を受け入れてもらえませんでしたが、電子本は受け入れてもらえました。これが最低限続くべきということですね。そして、できれば受け入れてもらえなかった地域図書館や出身大学図書館でも電子本ぐらいは受け入れてもらえるようになる…というのが Claude さんが示す方向なのだと思います。＜
JRF2026/9/134891
……。
追記。
○ 2026-09-12T16:38:13Z
AIアラインメント税(参: [cocolog:96128710](2026年8月)・[cocolog:96108909](2026年8月)の秩序からすれば、最終的には計算機を差し押さえることが必要なのであり、それは究極的には軍の役目なのだ。
学会が真実の探求を止める権限を持つとは、短絡すれば、学会が直に軍に命令できるのを許すようなものだ。そうあってはならない。あくまで、軍を動かすのは政府の役割でないといけない。学会は政府の諮問機関に留まるべきなのだ。
JRF2026/9/130809
だからおそらく Lean のライブラリへの登録などを学会に直接禁じられるようにさせるというのは方向が違う。ライブラリへのブロックを民間が・国家ができることのほうがきっと大事なのだと思う。学会はライブラリの階層を決めることぐらいはしてもいいのかもしれないが。
JRF2026/9/137707
……。
……。
追記。
○ 2026-09-13T12:28:43Z
数学界とAIの問題。意味のある証明、群論などの理論が途中で出来るという話。私の場合はラムダ計算の証明において人間にわかりやすい証明が自動証明では「効率的」でないという形で現れた。「わかりやすい証明」が評価されがたい。しかし、命題の表現力を高めて人間にフレンドリーにする…例えばオブジェクト指向を使って…などの必要性はあると私は考えていた。その過程で「わかりやすい証明」にも意味が出るだろう…と。実際は、命題の表現力を高めるより、人間がコンピュータの記号に慣れるような方向に行った気がする。どちらかというと。
JRF2026/9/143129
○ 2026-09-13T12:44:14Z
「わかりやすい証明」にAIはもちろん貢献できると思う。ただ、わかりやすさは教育(過程)によっても作られる…という側面もある。そういう意味では「政治的」で、そこに監査=注意労働のヒントがあるのかもしれない。
JRF2026/9/143067
(Claude Sonnet 5 さん、(出てこないけど)Grok 4.6(?) さん、ChatGPT 5.6 Luna(?) さん、Gemini 3.6 Flash さんと会話しながら。)
JRF2026/9/128201