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. 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.…