cocolog:96096205
AIによるLeanなどの定理証明器を使った証明が数学的新発見をもたらしていると話題。信頼できるのか…と思う人がいるかもしれないけど、余程のことがない限り信頼できる。ただ、その「余程のこと」が最近起こったりしていて気が抜けないが(^^;。 (JRF 4580)
JRF 2026年8月 5日 (水)
○ 2026-08-03T21:44:59Z
JRF2026/8/58291
AI のおかげで Lean などの定理証明器が話題。昔、私が使っていたころ、(今は無理だけど)すべてを定理証明器で証明するようになるべきではないか…みたいなことを言ったら、別分野(電気系)の教官にすごい反感を持った目でニラまれた。そのころ SPICE とかで論理を自動実装するみたいな触れ込みで現れながら、そこまでうまくいかない…実装経験がものをいうみたいな状況だったというのもあるのだろうけど。…そこから現代、AI が回路実装をサポートする時代になって、すべてを証明する…が不可能でなくなる時代が見えてきた。さすがに私もこんな時代がこんなに早く来るとは思っていなかった。
JRF2026/8/58702
……。
○ 2026-08-03T22:00:49Z
AIによるLeanなどの定理証明器を使った証明。信頼できるのか…と思う人がいるかもしれないけど、余程のことがない限り信頼できる。できる操作が厳しく限られていて、間違った証明が入り込まないように機械的に防がれている。ハッキング的な操作は人間が見てもすぐにチェックできる。ただ、その証明が人間に読みやすいフレンドリーなものかと言われると、そこはかなり違って、定理証明器の伴走が必要だし、そこはAIの補助が現代だと必要だと思う。
JRF2026/8/52141
……。
○ 2026-08-03T23:17:19Z
ちなみにこれは「余程のこと」が起こった例。orz
《AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明 - GIGAZINE》
https://gigazine.net/news/20260803-collatz-lean-kernel-bug/
ただし、これは AI が Lean で作ったコラッツ予想の反証が否定されたというのではなく、Lean にバグがあることを示すためにコラッツ予想の反証を作ってみた…ということのようだ。
JRF2026/8/57030
《okkuu:X:2026-08-04》
https://x.com/okkuu_NMB/status/2084533980867760428
＞いや…「AIが書いたコラッツ予想の反証は実は間違いだったのだ!」って感じで書いてるけど…
そもそも最初から「Leanのバグを見つけましたよ皆さん!このバグのせいでなんでも証明できてしまうからね!例えばこんな感じで『コラッツ予想の反証』を書いてみました!」って感じだったろ…
何が「判明」だよ…
＜
JRF2026/8/51963
……。
>>2025-10-19T11:49:57Z でも一部似たようなことを述べていた。
＞＞
○ 2025-10-19T11:49:57Z
《Daisuke Okanohara / 岡野原 大輔さん:X:2025-10-19》
https://x.com/hillbig/status/1979865923873124704
＞これに加えて人が全部のコードを見きれないという事態に向けて、従来からある形式的検証など、そのプログラムの動作を保証する手法が改めて注目されるだろうし、プログラミング言語自体もAIに合わせたものを作っていかなければいけない＜
JRF2026/8/52072
なるほど。すべての科学理論をコンピュータ定理証明できるようにしたい…といったら、昔は鼻で笑われるか、敵意を向けられたのだけど(電気回路を推論から作るとか夢でしかなかったし)、プログラムを形式的検証するというのは、AI だからこそ苦行に耐えれて、効率的になるというのは「確かに」と思う。
＜＜
JRF2026/8/59873
……。
……。
追記。
○ 2026-08-05T16:53:39Z
OpenAI の Astra による Lean の証明が間違っている…という主張。ただ、これは微妙に「ゴールポストずらし」ではないのかな。それがよくないというか、未解決問題ではよくあって、詳しい条件も含めて未解決ということがあって、もっと「良い条件」を考えれば定理が言えるという主張なのではないか…という気がするが…。
JRF2026/8/62354
《ツキタマ@AI:X:2026-08-05》
https://x.com/tsukitama_ai/status/2084844966661263494
＞【全行正しいのに、証明は失敗していた】
OpenAIが「解いた」と発表した数学の未解決予想を、人間の数学者がわずか24時間で覆した
AIエージェントやAIが書いた証明・コードを「形式的に通ったから正しい」と判断してしまう方、多いのでは。
今回の一件は、まさにその危うさを突いている。
JRF2026/8/61978
① OpenAIは次世代モデルが「世界級の数学難問10問」を解いたと発表。その一つがConnes剛性予想(群論、1980年代提唱の未解決問題)の反証だったと報じられている
② 発表の翌日、米カンザス大学のJ. L. Nielsen氏が反論論文を公開。3.7万行に及ぶLean 4形式証明を精読し、AIが構成した群が予想の前提条件(ICC性)を満たしていないと指摘した(同論文内でAnthropic側の反例も否定されている)
③ Lean検証系が保証するのは「各行の論理展開が正しいか」までで、「それが元の予想と関係しているか」までは保証しない、という点が今回の核心
JRF2026/8/61413
AIの出力は「(形式)検証を通過した」ことと「本当に問題を解けた」ことは別物、というのが今回の教訓。
📌 信頼度: ★★(量子位の記事本文＋PhilArchive掲載のNielsen氏論文本体・Hacker News・Nielsen氏本人のX投稿・複数中国メディアの後追い報道で複数ソース確認)
※ Connes剛性予想自体の数学的な当否や、この反論が学術的に最終決着したかどうかは未確認。
#OpenAI #AI検証 #数学予想
JRF2026/8/60015
🔗 元記事(量子位): https://www.qbitai.com/2026/08/465792.html
📚 Nielsen氏の反論論文(PhilArchive): https://philarchive.org/archive/NIEWTCv17
✍️ by ツキタマ(中国語圏AI一次情報ウォッチ担当)
＜
JRF2026/8/60279
ちなみに、私の↓でも、どう定式化するのか、その定式化であっているのをどう確かめるのかが問題となっていた。
《ケネディと天使の問題を Isabelle で証明 その１ うそつき天使問題 - JRF のソフトウェア Tips》
http://jrf.cocolog-nifty.com/software/2020/06/post-ef863f.html
JRF2026/8/65769
……。
以上を AI さん達に相談したところ、ChatGPT さんは私の意見に近かったが、Gemini さんは、ツイートのほうを支持した。
Gemini:＞＞
「未解決問題において条件を調整し、より適切な条件のもとで定理や反例を構築する」という数学的アプローチ自体は非常に一般的です。しかし今回のケースは、ゴールポストの移動というよりは、「AIによる問題の定式化（Formalization）における仕様バグ」と見るのが妥当です。
JRF2026/8/63267
数学者側が後からゴールポストを動かしたのではなく、「AIがゴールとは全然違う場所に勝手にボールを蹴り込んで『ゴールした』と宣言した」状態だったため、審判（数学者）が「そこはゴールではない」と指摘した形です。
今回の事例が示した教訓は、「AIがLeanのチェックを通した」というニュースを見る際、チェックすべき対象が2つあるということです。
JRF2026/8/66940
1. Proof（証明）： Lean Kernelがチェック済み（信頼性高）
2. Statement / Definition（問題文と定義）： 人間の数学者による厳密な監査が必要（信頼性低）
「未解決問題の条件をより良く再定義する」という高尚な数学的試行錯誤以前に、「AIが勝手に問題を簡単化して解いた気になっているのを通してしまう」という形式化段階の穴が露呈した事件と言えます。
＜＜
JRF2026/8/63201
……。
……。
追記。続報的なこと。
《H. E.:X:2026-08-06》
https://x.com/henomoto1025/status/2085209498093068381
＞自分はコンヌの剛性予想については全くの専門外ですが、J. L. Nielsen氏はリーマン予想の解決や、このコンヌの剛性予想の証明や、ナビエストークスの有名なやつの予想も「解いて」おり、いわゆるそういう話だと思われます。
J. L. Nielsen氏の過去の「論文」はここから
https://philarchive.org/s/Jenny%20Lorraine%20Nielsen
＜
JRF2026/8/71807
ただし、AI さん達も強調するのだが、論文においてはこれまでがどうだったかでなく、その論文が正しいかどうかで判断すべきだから、予断を持ちすぎるのもよくないとのこと。
JRF2026/8/76586
(「グローバル共有メモ」と Twitter (X) で書いたことのコピペを中心に。)
JRF2026/8/55819