AI ‘Disproves’ 90-Year-Old Math Problem: The Proof Assistant Was Broken First

In late July, an AI claimed to have overthrown the Collatz conjecture—a math problem that has baffled mathematicians for nearly 90 years. It offered a machine-checkable proof verified line by line by computer, looking virtually airtight. But before the world could celebrate, the truth emerged: the supposed counterexample was an illusion spawned by a soundness vulnerability in the proof verification tool itself. Ironical, given that the entire purpose of such tools is to eliminate AI hallucinations.

This story deserves to be understood from the beginning. It touches on a question we are all collectively betting on: How much can we really trust what AI tells us?

Understanding the 90-Year-Old Problem

The rules of the Collatz conjecture are so simple that even an elementary school student can understand them: Pick any positive integer. If it is even, divide it by 2; if it is odd, multiply it by 3 and add 1. Then repeat the process with the result.

For example, start with 6. Since 6 is even, divide by 2 to get 3. 3 is odd, so multiply by 3 and add 1 to get 10. 10 is even, so divide by 2 to get 5. 5 is odd, so 5 * 3 + 1 = 16. Then 16 -> 8 -> 4 -> 2 -> 1. What happens at 1? 1 is odd, so 1 * 3 + 1 brings us back to 4, entering an infinite loop of 4-2-1. The question is simply: No matter which number you start with, do you always end up in this 4-2-1 loop?

Posed by German mathematician Lothar Collatz in 1937, the problem remains unproven, and no counterexample has ever been found. Computers have tested every number up to (2^{68}) (about 295 quintillion), and every single one returned to 1. Yet mathematicians remain unimpressed—checking trillions of numbers is not a proof, just as observing billions of white swans does not prove that all swans are white. The legendary Hungarian mathematician Paul Erdős famously remarked: “Mathematics may not be ready for such problems.” The difficulty lies in its deceptive simplicity—simple rules, yet elusive as an eel.

Figure: The Collatz conjecture number tree—all numbers that reach 1 within 20 steps hang on this tree. Source: Wikipedia (All Collatz sequences of a length inferior to 20)

How the AI “Breakthrough” Was Baked

On July 25, computer scientist Raman Kumar released a code repository containing a purported “disproof”: a specific large number that allegedly never returns to 1, overthrowing the conjecture outright. The key selling point was that this disproof was a machine-verifiable proof generated with AI assistance.

To understand why this mattered, one needs to grasp a core concept in modern formal mathematics. In recent years, a practice has taken hold of writing mathematical proofs as code in specialized programming languages and submitting them to a “proof compiler” like Lean. Lean acts as an unforgiving examiner: it breaks down every step of a proof, checking line by line. If any step skips logical rigor, it immediately throws a red flag and rejects it. A proof passed by Lean is theoretically impossible to be wrong—and that is its explicit design goal: replacing human reviewer oversight and bias with uncompromising machine validation.

This tool carries immense weight across tech: security kernels of operating systems, underlying protocols of cryptocurrencies, and tens of thousands of mathematical theorems rely on machine verification. The industry has even touted it as the ultimate cure for “AI hallucination”: it doesn’t matter if the AI makes things up, as long as the machine acts as the final gatekeeper.

So when Kumar presented a “Lean-verified counterexample,” experts were initially stunned. If the proof truly passed machine inspection, a 90-year-old math milestone had collapsed. News spread rapidly across social media under glowing headlines: “AI Overthrows 90-Year-Old Math Problem.”

The Truth: The Grader Made a Grading Error

The plot twist arrived swiftly. On July 28, another researcher reduced the counterexample to a minimal logical contradiction and opened an official issue on Lean’s repository, tagged as bug #14576. The issue title was chillingly concise: “kernel accepts ill-typed projection, allowing proof of false without premises.”

In plain terms: the supposedly flawless grader had skipped a check in its core validation logic. When validating nested data types, a step failed to verify whether type names matched. As a result, an illegal structural component hidden inside the AI-generated proof slipped right through the crack. The moment the machine declared “verified,” it was merely rubber-stamping an illusion.

Figure: Orbits of small numbers under Collatz rules, all converging to 1. Source: Wikipedia (Collatz graph, skipping 27)

Then came the most dramatic twist of all. The Lean community has long maintained a “double insurance” design: alongside the official kernel grader, there is an independent third-party checker (written in a different language by a separate team) designed to cross-check official results. This independence assumption serves as the fuse for the entire trust chain of machine verification.

This time, the fuse blew. Subsequent postmortem analysis confirmed that two unrelated bugs had to be hit simultaneously: the official kernel missed the nested type check, while the independent verifier had a flaw in its projection checking. Hidden in separate corners of two different codebases, both bugs were triggered by the exact same “disproof.” The flaw in the independent verifier had actually been fixed just a week prior, but the AI happened to use a pre-fix version. Lean’s creator, Leo de Moura, noted candidly in his postmortem that while the author believed the timing was coincidental, one could not rule out the possibility that the AI had seen the bug report in its training data.

How should this be interpreted from an engineering perspective? Having two independent implementations pierced by the exact same bullet carries an astronomically low probability—implying either extreme bad luck or that the “disproof” was crafted specifically around the vulnerability. De Moura gave his own assessment: “This type of event will continue to happen. AIs are extremely effective at exploiting soundness bugs in kernels.” The bug was patched and deployed within an hour of submission, proving the kernel architecture itself is healthy; yet discovering it required a headline-grabbing “AI breakthrough.”

Who Verifies the Verifier?

The aftermath of this incident is even more thought-provoking than the event itself. After the flaw was discovered, OpenAI dispatched a cybersecurity AI researcher to assist in auditing the Lean kernel, unearthing several other programming errors—all of which were promptly fixed. In other words: the tool designed to guard against AI now relies on AI to catch its own bugs.

Meanwhile, the “Lean-in-Lean” project (which aims to write and verify the checker inside Lean itself) has not yet covered the problematic code path, and the ported code snippet contained the exact same bug. Verification is layered: AI outputs rely on verifiers, verifiers rely on independent second implementations, but who checks the second implementation? Each layer adds an extra step and cost, but there is never a “final layer.” This aligns with engineering reality: “machine verified” is always a probabilistic attribute—the deeper and more independent the checks, the lower the probability of error, but it is never absolute zero.

For the general public, the primary takeaway is calibrating expectations. Next time a headline proclaims “AI Solves Century-Old Math Problem” or “AI Proves Theorem,” ask one more question: Was it verified by humans or machines? If by machine, has that machine itself been verified? Conversely, there is no need to sink into nihilistic skepticism. Math itself emerged completely unscathed; the Collatz conjecture still stands firm. The bug was disclosed, fixed, and documented in a textbook postmortem. The system had a bug, but the way it digested and fixed the bug is precisely why it earns our trust.

Trust is a chain where any link might break. Smart observers don’t pretend the chain is unbroken; they simply remember to audit each link regularly. This time, AI found a crack in one of those links for us—by way of a false breakthrough.

Reference Links:

• Leo de Moura’s Postmortem: Full Postmortem for Kernel Soundness Bug #14576
• Lobsters Discussion (ojcl8j): Community Discussion on Kernel Soundness Bug (48 points)
• Wikipedia: Collatz Conjecture (Rules, History, and Verification Progress)