flâneur

Why is it all in the kernel?

lawrencecpaulson.github.io · 1,089 words · saved by 1 readers

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! 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 failed to find a single count

30 Jul 2026 [ general Lean Isabelle HOL system philosophy memories ] 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.…

saved by

related reading