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! 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
- Human mathematicians are being outcounterexampledxenaproject.wordpress.com
- Formalizing Fermat's Last Theoremanthropic.com
- A shallow dive into formal verificationvitalik.eth.limo
- Shtetl-Optimized >> Blog Archive >> Ten Signs a Claimed Mathematical Breakthrough is Wrongscottaaronson.blog
- cs.stanford.edu/~knuth/papers/claude-cycles.pdfcs.stanford.edu
- FLT: Anthropic has beaten me to itxenaproject.wordpress.com
- A Theory That Proves Its Own Inconsistency · Yan Sheng's siteangyansheng.github.io
- I believe P=NPemanueleviola.wordpress.com
- Reasons to believescottaaronson.blog
- When AI Writes the World's Software, Who Verifies It? — Leonardo de Mouraleodemoura.github.io
- "Why don't you use dependent types?"lawrencecpaulson.github.io
- Broken proofs and broken proverslawrencecpaulson.github.io