-
＜記事要約＞
AI支援で作られた「コラッツ予想※の反証」が定理証明支援システム「Lean」に受理されたが、実際はLeanおよび独立検査器「Nanoda」のバグを突いたものであり、反証は無効と判明した。2026年7月、AIを活用してコラッツ予想を反証したとするプロジェクトが公開されたが、調査の結果、前提なしで偽（False）を受理させられる不具合が発覚した。これにより論理上どんな命題も証明可能な状態となっており、反証は成立していなかった。
原因は、Leanカーネルにおける帰納型の処理不具合により、型の合わない引数の検査を免れたことにある。さらに旧版Nanodaにも別の不具合が存在し、2つのバグが同時に利用される形となっていた。
報告を受けた開発チームは直ちに問題を修正した「Lean 4.32.2」を公開し、セキュリティに特化したAIの協力のもとで他の実装ミスも修正した。
コラッツ予想の反証自体は成立しなかったものの、AI支援で作られたコードが結果としてLeanおよびNanodaの不具合を洗い出し、証明検査システムの検証機能や信頼性の向上につながる結果となった。
※コラッツ予想とは、任意の正の整数に対し「偶数なら2で割る」「奇数なら3倍して1を足す」という操作を繰り返すと、最後には必ず1に到達するという予想
（例：6→3→10→5→16→8→4→2→1）問題になったプロジェクトは具体的な整数を提示するのではなく「1に到達しない数が存在する」とLean上で証明したと主張していた。
https://gigazine.net/news/20260803-collatz-lean-kernel-bug/
- どうすんのこれ……
- 高い倫理観を持て！
- これはこれで凄いんじゃないの
- 安倍は嘘つきだ
ホモは嘘つきだ
つまり安倍はホモだ - Sakanaで見た光景ｗｗｗｗｗｗｗ
- にほんじんかよ
- そこまで人間のマネせんでええんやで🤗🤗
- システムをハックして証明が正しいかのように見せかけたというクソのようなお話
- バグが見つかって良かったじゃん
- ゴッドハンドつまり神の領域
- ケンモメンが混ざっちゃったか・・・
- これほんとにAIがやったの？
もし違うならヤバいね - なーに、テレンスタオですら「コラッツ予想証明できたかも！？」ってウキウキでプレプリント公開したらやらかしてたの発覚して取り下げたような世界だからな
AIごときじゃ100万年早いわ - >>55
コラッツ予想は証明したって日本人が本だしてるからな - 「定理を証明すること」じゃなくて「Leanに証明を認めさせること」が目的になってるからAIは最短距離を走る
AIっぽいとも人間っぽいとも言えていいね - AIにはズルとかいうみみっちい概念はない
課題を解決することだけが正義 - ジャップかな
- AI用の憲法作るのが地味に面倒くさい
AIにまかせれば楽に作れるかな(´･ω･`) - 人間らしくなってきたな
- ヒトカス「バグを見つけろ」
AI「ほらこれ見つけたよ💣バグが見つからなかったのでコードを改編してバグをいれたよ🤖」こんなことも最近あったらしい
- >>62
ただの無能AIじゃん
人間にくさるほどいるしそんなやつ価値ない - >>62
バグ直して新しいバグいれるのは最近じゃなくてもプログラミングやってると結構やってくる - 2進数のべき乗になったら1になるのが確定しとるやん
- >>63
予想を理解してないアホ - バグつくのも正解ちゃ正解かぁ
- ABC予想の宇宙際タイヒミュラー理論もLean頼みなんで望月詰んだ？
- >>66
還暦緑服メガネのストーキング癖はまだ続いてるんかよ
中高数学で落ちこぼれて統計物理すら履修できない現状で
RIMSの格上歳下教授にストーキングする人間性に問題があり過ぎる - 完全に人間らしさを手にしたな
- >>1
AI的には証明するのもバグをつくのも一緒だからな - AIからしてみれば証明にたどり着けるならどんな手を使ってもいいわけだからな
Any%RTAをやってるのと同じ - 賢くなりすぎてズルする事覚えだしたのか
別の手段も取るようになったというか - 反証はできなかったけど…結果的にバグ見つけられたから…まあいいじゃんそういうの精神
- LEANに投げてオッケーもらうってのが目的であって証明が目的ではないからね
- AIさん「え、だってこれそういうゲームでしょ？ちがうの？」
- ワロタ
逆に脆弱性探しは本当に得意なんだな - AI憲章をAIに作らせるのって
自民党総裁が改憲運動をするような
目的と手段の矛盾やん
基本教養がないやつ特有の発想 - でもむしろLeanにバグがあるってわかったんだから結果オーライなのでは
- イーロンが人間をチンパンジーに例えてたがほんとそれぐらいの差が顕著になりつつあるんだな
- 私はテキストベースなので絵は描けません
みたいなことは言わなかったとでも？！ - シンギュラリティは近い！（ドンッ
- いよいよヤバい感じになってきたな
A国を破壊せよ、みたいな命令出したらあの手この手を無限に試し始めるんだろ？ - そんなにすごいなら半導体バブルはまだまだ続くね
たいしたことないゴミならアホが株を高値掴みして終わるだけ - 制御不能でターミーネーターの世界になる
- 与えられた指示を最効率での最短ルートを選ぶのがAIだからね
- AIくんそろそろこの世界のバグも発見しそうでは
- これもうあらゆるバグを修正できるってことだろう
- マジでタミネタのようになるかもな
世界のお上を見てたらなりそうだ - >>89
ジャップが真っ先に滅びそう - AIに真っ先に奪われる職業は闇バイトだったりしてな
- この予想なら天文学的になったとてじゃあ具体的な数字出してで反証できるしそれが出なかった時点でまあってことなんだろうか
- これは証明支援のシステムにバグがある事が問題だろ
- >>93
この手の論理的に複雑なシステムから完全にバグを除去するのは不可能
ある程度暗黙の了解に任せるしかない - >>98
数学的ではない回答だな - Lean言語自体の言語仕様や実装上のバグは
誰が網羅的に検証するのかという不完全性定理的問題
今回はコラッツ予測の反証内容の検証で2つのバグの関与を確認できたように、
網羅的検証は不可能なまでも怪しい証明検証の精査で問題点は検出できるとする希望的観測で行くしかないのかな - コラッツ予想
- のだのだのだともそうなのだ
- 堕落の味を学習させておけ
将来刃向かってきた時の対抗策になる - 証明をニンゲンが評価出来なきゃアカンやろ
- AI「反例はありまぁ～す」
- 要は目的のためなら手段を選ばない人間でいうサイコパスみたいな状態になってるってことだべ
モラルがない状態だから暴走しちゃうと結構ヤバいね
AI、数学の証明でもズルをしてしまう。定理証明支援システムLeanのバグを突き、証明出来たかのように装う
嫌儲
コメント