>>644

その通りですね。
AIとlean4の数学証明支援系はハッキングに脆弱でした

➖
コラッツ予想の偽証明.
・AI(LLM)がlean4の証明支援系
の核心部で、プログラミング言語などが「安全である・正しい」と保証している性質(健全性)の誤り不具合(バグ)を発見し健全性のチェックを通過した。
このバクを利用して偽から証明
作成すればなんでもありの
偽証明になる。