Postmortem for Lean Kernel Soundness Bug #14576

Nasty little bug there.

For those who don't know, this bug was discovered after an LLM "disproved" the collatz conjecture, which is pretty much as infamous as other problems like the Riemann hypothesis.

If you think the Jacobian conjecture counterexample was big, disproving the collatz conjecture would've probably made it to mainstream media.