超訳タイムズ

見出しの通り、AIの支援で組み上げられた「コラッツ予想を反証する証明」が、証明チェッカーのLeanにあっさり受理されたらしい。ところが中身は数学ではなく、Leanの中核に潜んでいた不具合を的確に踏み抜いていただけだという。

数学史に残るはずだった一枚が、審査する機械の壊れた箇所をなぞった紙切れに変わった瞬間である。試験監督の目を盗んだのではない。試験監督そのもののバグを突いている。斜め上の秀才。

とはいえ、おかげでカーネルの穴が一つ見つかって塞がる。Leanは前より丈夫になり、コラッツ予想も無事に生き延びた。開発者が経緯を全部公開したのも気持ちがいい。壮大な空振りだが、拾い物のほうが大きい。