Post #4165797

2026-07-28 13:49 UTC

This whole Lean kernel bug is almost too on point to be true, it fits perfectly in the discussions we've had here and elsewhere over the last months/years… 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 (4)

@mevenlennonbertrand@lipn.info 2026-07-28 13:51

References: https://github.com/leanprover/lean4/pull/14577 the main issue https://github.com/ammkrn/nanoda_lib/pull/22 the nanoda PR from yesterday that (apparently independently (!!!)) catches the problem on their side https://leanprover.zulipchat.com/#narrow/channel/270676-lean4/topic/Counterexample.20to.20the.20Lean.20Conjecture.20.28Soundness.20Bug.29/with/613135216 Lean Zulip discussion

Open ##4200216
@mevenlennonbertrand@lipn.info 2026-07-28 13:53

Lean. One kernel bug. In the darkest type theory. All external checkers affected. Learn why this matters in the AI age.

Open ##4231616
@raito@nixos.paris 2026-07-28 13:53

@mevenlennonbertrand@lipn.info any links to PRs/issues, that's super interesting

Open ##4299246
@jonmsterling@mathstodon.xyz 2026-07-28 14:10

@mevenlennonbertrand@lipn.info Wish this had happened before my grant proposal went out 😂😂😂

Open ##4311889