2026年08月03日 21時00分 AI
AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明
https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

こういうことがあるから、定理の証明系システムも正しいことを機械的に証明しなければならんし、
それを動かしている言語処理系、OS、CPU、ハードウェア、すべてが無欠陥であることを証明しなけ
ればならない。