I built a 9,000-Line Proof Assistant Formalization of the Collatz Conjecture in Lean 4, so you don’t have to.

The Solenoid Sieve: How I “Saw” the Collatz Conjecture Without a Mind’s Eye

For over a century, the Collatz Conjecture has been the “black hole” of mathematics. It is a problem so simple a child can understand it, yet so structurally deep that it has defeated the greatest minds of the 20th century. Paul Erdős famously said, “Mathematics is not yet ready for such problems.” It has defeated every approach thrown at it for nearly …