Post #4168178

2026-07-28 16:15 UTC

As an interesting follow-up to the ai-does-maths-using lean4 stubstack comments on Sunday, an llm accidentally uncovers a bug in the lean4 kernel. Summary by lipn.info/…/116997917683191056 To summarize: an AI agent let loose provides a sorry-free proof of the Collatz conjecture the proof is detected as actually being a kernel bug the bug is related to (nested) inductive types, for which there is no clear theoretical specification: the kernel’s code is the reference external checkers (lean4lean and nanoda from a week ago) reproduce the bug, because they essentially copied the reference kernel implementation And so AI raises the bar for kernel correctness by a lot without a clear type-theoretic understanding of what is actually implemented, we’re toast external checkers help to catch implementation bugs, but without a clear specification they can’t catch logic bugs

Replies (2)

@corbin@awful.systems 2026-07-28 17:20

Lean was already known to be untrustworthy and bad, although people refuse to internalize the situation because they’re caught up in Buzzard’s hype machine. This is extremely funny but I don’t see any signs of people waking up and realizing that Lean sucks.

Open ##4169463
@rook@awful.systems 2026-07-29 10:24

A little bit of plot thickening spotted by abadidea: infosec.exchange/@0xabad1dea/117002106099986943 tl;dr, the timeline looks like this: “proof” of collatz conjecture released bugs identified in lean kernel proof demonstrated to use these bugs There was only a day between the first two events, and the non-proof was not where the bugs were discovered. So maybe it was just a coincidence that the chatbot found the bug at the same time, or maybe it’s training data included previous investigations into those bugs which it then built upon and that would be a bad thing for other llm generated proofs. The collatz conjecture is sufficiently famous that enough third-party checking was done to sort the problem. I wonder how much checking would have been done on proofs of less famous and interesting things.

Open ##4193509