technology
Lean fixes kernel bug exposed by an invalid Collatz disproof
Lean fixed a soundness bug in its kernel after an invalid, AI-assisted Collatz disproof exposed a path to making it accept a proof of False. The postmortem describes a separate flaw in an older independent checker and the fixes and safeguards that followed.