Postmortem for Kernel Soundness Bug #14576

The implementation of the kernel is relatively trivial, it's an intentional design choice.

> much simpler type checkers like Rust's

Linear/Affine types aren't easy, although deep down it is about enforcing XOR.

To what degree can you say something like "if the kernel doesn't have metaprogramming [or some other set of features] it's fine". When were the last bugs with a reduced feature set?

I think this rates as too obvious to say among anyone remotely close to this, but worth noting there is a lot of distance between an exploit and any real confusion.

Proofs aren't generally machine-read-only. An exploit of a proof system kernel doesn't necessarily look like normal proof code. Exploits can be fragile: 'safe' tweaks break them. If an exploit used maliciously is found, the person sneaking it through wouldn't exactly be thanked for it. And the window for exploits overall seems to be shrinking: Lean/nanoda are easier to secure than, say, Chrome.

If someone wanted to deliberately sow confusion (my career advice is not to do that!) they would probably have better luck with a subtly wrong formalization or an informal proof. If they have prover kernel bugs, they should report them and get free T-shirts.

Still, it's cool to see how they're hardening Lean.

Took me about 90 seconds to find a Metamath implementation bug that apparently allowed proving something that shouldn't be provable: https://github.com/metamath/metamath-exe/issues/184

The utility of autoformalization is not actually in confirming the correctness of human-checked results. Mathematicians have a pretty good peer review process. I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect -- though I'm sure cases exist, it's astoundingly rare.

The mathematics community's motivation for formalizing problems like Maryna Viazovska's sphere packing results in Lean weren't because the results were in doubt -- she won a Fields Medal for it, it's an extremely examined proof -- but because formalizing those results would lead to a lot of interesting and useful mathematical objects needing to be formalized as a prerequisite, which could then be merged into Lean's Mathlib and become useful for anyone working with Lean, particularly students. Having a library of idiomatic proofs available in a formal system capable of checking your work is Really Cool! Working in a proof assistant is a great way to develop mathematical maturity, especially for people who might not have an undergraduate education available to them.

(Unfortunately in the sphere packing case, the research group working on it made the mistake of trusting one of the various "AI for Math" slop companies, who promptly rugpulled them: https://arxiv.org/html/2603.03684v3)

So the short answer is "it depends on what you want". Lean is an eminently usable system for humans and LLMs alike; Metamath is uh. Not. But yes, Metamath seems to have a more trustable kernel wrt. the independent verifiers, so if that's all you're after it would be a better pick. But... there's only so many bugs Lean's kernel can have. At some point, they'll all be found.

We want Lean4 (or any other deduction system that we use, for that matter) to be correct, i.e. "what is a true statement" and "what is a derivable statement" should be the same.

"every statement that can be derived also holds" is the difficult part to show, and something we refer to as soundness. For some fancy logics, it's not even possible to show, hence the discovered Kernel Soundness Bug in Lean!

"every statement that holds can also be derived", a notion known as completeness, is often a trivial property; in practice, we use refutation completeness instead, i.e. "every statement that doesn't hold can derive false". A bug that would allow a user to prove/derive a previously unproven statement would fall under this category of "completeness bug".

However, such completeness bugs immediately show up in testing. Generally, deduction systems have two kinds of rules: a handful of rules that are enough to establish (refutation) completeness, and then a few extra rules to optimize inference. Because so few rules are needed for completeness, lots of test cases will break if one of the rules break.

--

I'm not actually sure how the completeness situation looks like for proper provers like Lean. It's my graduate student's hubris to assume completeness remains easy to show for more advanced systems than the Superposition calculus ;)

A correctness bug in a proof checker by definition means that you can prove false.

A counterexample of the form "X cycles to X after N steps" is easy to check. A counterexample of the form "starting with X we keep going up forever" is hard to check in finite time.

No, Lean allows non-constructive proofs so a proof could be like "if the Riemann hypothesis is true the counterexample is 42 otherwise it is the first nontrivial zero" or something like this, and then you don't get a fully closed counterexample.

This was never about the Collatz conjecture itself. If I understand the original discussion correctly (as of a few days ago, not sure if new stuff has come to light), everybody agreed that that framing was just a flashy gimmick. And some Lean maintainers were unhappy about it, since this framing just added noise to the reproducer; they would have preferred a simple proof of False. Nobody ever thought that the disproof might be real.

This had nothing to do with Collatz and everything to do with a Lean bug.

The proof was not actually a proof at all, because it was unsound (despite Lean admitting the proof).

Trust in formal reasoning is necessarily always conditional. You have to start somewhere. The good thing about verified formal proofs is that the only way they can be in error is if the verifier is faulty. This drastically limits the possible reasons for error.

(In practice, there’s also the possible error that the proved formal statement means something different than what you thought it meant.)

One can only trust a verifier as far as they can trust anything made out of software.

I would expect proofs that exploit kernel bugs to look fishy, so someone reading the proof could catch the smell.

That said, I'm sure there's also room for underhanded Lean programming as well, which would be even more interesting.

It has nothing to do with LLMs. One cannot trust the proof of anything if one cannot trust the verifier.

The relevant kernel code isn't written by Claude though. According to git blame, 95% of the code in inductive.cpp is 5+ years old, with only ~3 hunks (totaling less than 30 lines) coming within the last 12 months including this fix. The Lean kernel in general does not seem to change very much, e.g. the last two years are very sparse in terms of activity with relatively contained changes when I examine the history (especially so when contrasted with the pace of the rest of the project).

Beyond that it looks like a pretty simple oversight. Coq and Isabelle have also had 'prove False' bugs, it isn't the end of the world. Stuff like this happens.

What is the error rate of human programmers? Anyone who tells you that either human or A.I. code is magically exempt from issues is selling you something.

Do you have any evidence that the bugs were due to LLM code? Or are you just speculating baselessly