・AI支援で作られた「コラッツ予想の反証」は無効、Leanのカーネルバグを突いていたことが判明

https://gigazine.net/news/20260803-collatz-lean-kernel-bug/

・『Lean で証明できた』は何を保証するのか？ 〜 Lean の無矛盾性と信頼の根拠 〜

https://qiita.com/kyamaz/items/7b38e5977dc97747d2d9


・Postmortem for Kernel Soundness Bug #14576

> Verification 確認
Mario Carneiro's lean4lean is a Lean formalization of Lean's type theory together with a proof that the kernel implements it.
The work is ongoing, the proof of consistency does not cover inductive types yet, and the to-be-verified implementation suffered from the same bug as the official kernel. The bug would have been found when attempting to conclude the verification of this part.

https://leodemoura.github.io/blog/2026-8-1-postmortem-for-kernel-soundness-bug-14576/