News · 2026-09-30

The Collatz artifact passed two buggy checkers; the conjecture remains open

An AI-assisted artifact that appeared to refute the Collatz conjecture was accepted by two proof checkers because each contained a different implementation bug. The incident dates to July and received renewed attention in a September 29 interview; it did not disprove Collatz. Lean’s primary issue records and Leonardo de Moura’s postmortem explain why a machine-checked result still depends on the checker version and the integrity of the verification boundary.

Key facts

• Two distinct checker bugs allowed the same hostile artifact to pass.
• Lean issue #14576 and its fix date to July 28, 2026.
• The affected independent nanoda build was older; its fix merged July 27.
• Primary source: Leonardo de Moura’s kernel-soundness postmortem.

Collatz asks whether repeatedly applying a simple rule to a positive integer always eventually reaches one. A genuine counterexample would be a major mathematical result. This episode instead demonstrated something about software: an artifact can be accepted by a faulty verifier even when it proves no valid theorem. Calling that a disproof confuses the certificate’s claimed content with the program’s decision to accept it.

A proof assistant separates the machinery that constructs a proof from a small trusted component that checks it. The construction layer is allowed to be complex, experimental, or even hostile. The checker must reject malformed declarations regardless of how they arrive. The attraction for AI-generated mathematics is that plausible language can be replaced with a concrete term that a machine examines. The residual risk moves into the trusted implementation and the exact statement being checked.

The Lean issue exposes the boundary crossing. The hostile artifact used metaprogramming to send a declaration directly to the kernel. In nested-inductive processing, parameters absent from constructor fields were dropped from generated auxiliary declarations and escaped the required type checking. Kiran Gopinathan reduced the problem to an axiom-free proof of False. A verifier accepting False is a software-soundness failure, not a surprising new law of mathematics.

The Lean fix merged on July 28. The independent Rust checker nanoda had another defect: it failed to verify the structure name recorded in a projection node. A crafted projection named a structure that did not match the value’s actual type. Its fix pull request merged July 27. The successful artifact used an older nanoda build. These mechanisms and dates should remain separate rather than being retold as one shared checker bug.

The concrete analogy is a forged building permit that passes two desks for different reasons. One clerk omits a required signature check; the other accepts the wrong property identifier. Two approvals are more reassuring than one only when their checks are correct and their assumptions do not fail together. Implementation diversity reduces some risks but cannot turn a mistaken program into an infallible mathematical authority.

De Moura argues that removing metaprogramming is the wrong response. Lean’s construction machinery is intentionally untrusted; the kernel needs to defend its own boundary. A subsequent uniformity-check change strengthened inductive checking. A different August equality-cache fix addressed another soundness defect, reported using OpenAI’s internal models. The two exploits generated for that later issue were caught by independent checkers, showing why multiple implementations remain useful despite the July failure.

The practical workflow is comparator. It builds a proposed proof in a sandbox, exports the artifact, and validates and replays it against a trusted challenge statement outside that sandbox. External checkers can be included. The Lean reference manual calls comparator with external checkers the “gold standard” for high-risk validation. The manual still lists assumptions about the statement, the sandbox and plumbing, and bugs affecting the checkers.

The September interview made those trust assumptions timely for a broader AI audience, but its recalled timing does not supersede dated issue records. No new September Collatz discovery is established. Proposed checker bounties discussed in the interview were an idea rather than an announced program, and inaccessible discussion pages do not support a claim of expert consensus. The strongest evidence is the inspectable reproducer, patches, and postmortem.

For AI mathematics, the lesson is to publish the exact statement, proof artifact, versions, and independent replay procedure. Machine checking remains a powerful filter against convincing nonsense. This incident shows why adversarial tests must also target the filter itself, especially as models become capable of generating complicated inputs. The conjecture remains open; the verified development is improved understanding and repair of the software that might one day certify a valid proof.

Primary source, verified: read the paper →

Ground Truth. (2026, September 30). The Collatz artifact passed two buggy checkers; the conjecture remains open. Ground Truth. https://groundtruth.day/news/lean-collatz-checker-bugs-revisited.html

@misc{groundtruth:lean-collatz-checker-bugs-revisited,
  title  = {The Collatz artifact passed two buggy checkers; the conjecture remains open},
  author = {{Ground Truth}},
  year   = {2026},
  month  = {sep},
  url    = {https://groundtruth.day/news/lean-collatz-checker-bugs-revisited.html}
}

Topics: formal-verification · mathematics · ai-research · reliability