Why is it all in the kernel?

Sensational news! The Collatz conjecture has just been refuted. Ramana Kumar has proved its negation. The proof has been checked in Lean and double‑checked using the independent Nanoda type checker. Unfortunately, the proof is wrong. It exploited a bug in the Lean kernel. Somehow, Nanoda didn’t detect the error either. Now I am not writing to gloat about this. Soundness bugs have been discovered in Isabelle, among many other proof assistants; for all I know, a new and monstrous bug will be discovered tomorrow. Nevertheless, there are some lessons here, so let’s go! The Collatz conjecture This famous conjecture has been around for nearly a century, attracting the attention of serious mathematicians and cranks alike. It concerns the following procedure. Start with a number N. Now repeat this step: if N is even then divide it by two; if odd, set N to 3N+1. Collatz conjectured that this procedure is guaranteed to reach 1 no matter what value of N we start with. Extensive testing has…