Postmortem for Kernel Soundness Bug #14576
leodemoura.github.io> The practical consequence: checking with an independent kernel still works, since it required two distinct bugs in two implementations, but users who rely on it need current versions of both.
Things like this aren't too surprising, given that even much simpler type checkers like Rust's have soundness issues occasionally. I think it's very important to view verified results not as an absolute and unbreakable guarantee, just an extraordinarily strong one where (1) the surface area for soundness issues has been painstakingly minimized and (2) any realized soundness issues are taken very seriously and fixed in short order.
> much simpler type checkers like Rust's
Linear/Affine types aren't easy, although deep down it is about enforcing XOR.
The implementation of the kernel is relatively trivial, it's an intentional design choice.
As claude would say, "relatively" is carrying a lot of weight in that frase. Definitely load-bearing — would not pass a quick smoke test.
but where’s the seam!?
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?
Read the article. The elaborator (where metaprogramming is evaluated) is not part of the trusted computing base. The security model is that bad proof terms get rejected, not that they're never generated.
This thread has some context. A proof-system researcher found some proof-system bugs and presented them a funny way:
https://leanprover.zulipchat.com/#narrow/channel/270676-lean...
A mathematically-inclined reviewer (or an LLM) can quickly identify that it's an exploit. (Two exploits; it's crafted to hit a bug in another proof checker, too.)
The post gestures at this, but a natural follow-up, beyond fixing specific bugs around this exploit, would be to task some security-oriented models with proving False in Lean, or with reviewing the code for potentially unsound steps, missing checks, or even useful 'hardening'. That's happening and bugfixes are landing as a result.
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.
Feels appropriate for bugs in a formal proof system:
> Beware of bugs in the above code; I have only proved it correct, not tried it.
-Knuth, 1977
Reminds me of this: https://mathoverflow.net/questions/513742/are-we-stuck-with-...
I know this is an implementation bug not a meta-theory bug, but I'd almost consider the fact soundness bugs are possible as a bug in the ideology, or at least a severe drawback. Stuff like this just wouldn't happen in Metamath. In a future where AI is autogenerating formalizations, why not have the AI use a harder but airtight system like Metamath?
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
That's with the original C verifier only. The actual database is cross-checked by 6 independent implementations. This is the whole point of Metamath: its kernel is so tiny that you can implement a verifier in a weekend.
Metamath isn't a silver bullet in the design space of formal proof tools, but I personally think it just about nails the metatheory we want. Maybe some explicit facility around definitions would be desireable.
As it happens, the Python verifier mmverify.py has an even simpler soundness bug [0], and so far I've reviewed two independent AI-written verifiers that have replicated that bug, since they apparently really like to copy the strategy from mmverify.py. A sound verifier isn't too difficult to write in terms of architecture (I just wrote one myself for differential testing [1]), but it requires some close attention to the details.
That is to say, the Swiss-cheese approach definitely lends authority, but individual implementations are unfortunately not as foolproof as they're made out to be.
[0] https://github.com/david-a-wheeler/mmverify.py/issues/30
[1] https://github.com/LegionMammal978/mm-verifier-tests/blob/ma...
Why does the original C verifier have bugs if its supposedly so easy to implement a verifier?
Ease of implementation means we get more, independent verifiers rather than trusting any particular one.
Nothing more complex than Hello world is easy to implement in C without risking mistakes in checking boundary conditions if you are not really careful.
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.
(I should note that there is also utility in confirming the correctness of results that are too complex to be adequately verified by humans. The recent result that NF is consistent wrt. ZFC, among others (Peter Scholze's Liquid Tensors project) are examples of this. But that's distinct from "autoformalization" as commonly applied.)
> I'm not actually aware offhand of any mathematical results that were accepted and later found to be incorrect
https://mathoverflow.net/questions/35468/widely-accepted-mat...
Yes, in particular the slides by Kevin Buzzard (linked in there or here: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli... ) are funny and educational on that matter.
And everyone who's been into this stuff for a while has had their prediction come through.
If AI is water, Lean is the pipe and collatz is a clog on one end, then surely we'll find the cracks.
Has there ever been a bug that allowed to prove a previously unproven statement, without allowing the user to prove "false" by exploiting the bug directly?
If every bug-exploiting proof would make it easy to prove false, putting a bounty on proving false could increase trust in the validity of verified but obscure Lean proofs.
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 ;)
Don't Godel's incompleteness theorems mean that completeness is a property you don't want in a prover (as it means the prover must then be inconsistent and this unsuable) and consistency is a property of the prover you cannot prove using the prover itself?
>"what is a true statement" and "what is a derivable statement" should be the same.
you mention completeness in the rest of your comment, so I'm not sure how you aren't aware of this, but the famous incompleteness theorem says that for a consistent set of axioms there will always be true statements you can't prove.[1]
[1] https://en.wikipedia.org/wiki/Gödel%27s_incompleteness_theor...
That's not what it says. It says that as long as the logic is rich enough (first-order isn't enough) and consistent there are statements where neither the statement nor its negation is provable. You may choose to create a new logic by adding either the statement or its negation as an additional axiom, and it will (obviously?) remain consistent.
Truth is some sort of value judgment that is outside the scope of formal systems. And looking at how bizarre Gödel statements are, it's unclear if there's any particular justification for declaring them to be true or false.
The type theory of Lean is certainly rich enough though
err... There are always more ---> you can't make it "compete" by adding finite number of axioms
You can make it complete, it just won't be consistent.
In fact there is a simple way to do it -- add contradictory axioms and then you can use the principle of explosion to prove any statement as true. Is such a system inconsistent and thus useless? Yes, but it is complete.
The second paragraph of my link talks specifically about truth:
>The first incompleteness theorem states that no consistent system of axioms whose theorems can be listed by an effective procedure (i.e. an algorithm) is capable of proving all truths about the arithmetic of natural numbers. For any such consistent formal system, there will always be statements about natural numbers that are true, but that are unprovable within the system.
A correctness bug in a proof checker by definition means that you can prove false.
Not necessarily. For example, perhaps my ZFC first-order-logic theorem checker implicitly accidentally contains the continuum hypothesis as an axiom. This isn't inconsistent but it is a correctness bug.
(For that matter, another correctness bug is "the checker rejects all proofs". You can't prove false if you can't prove anything.)
good point, I didn't think about these cases.
But how obvious would that be in the proof? Especially when you don't know if the proven statement is not true/implies false. Afaik all past problematic Lean bugs clearly implied false. But could it be that a bug is used in a way that this is absolutely not clear?
For example, the bug could allow proving a=b if the hashes of the terms equal. And the only (hypothetically) known hash collision that could be used to exploit this might not lead to an obvious contradiction.
Let a and b be as you describe (hash collision), and suppose that collisions are extremely rare. We have a theorem that a=b => a+1=b+1. But in this case, a=b according to our hash-equality, but a+1!=b+1, which contradicts the theorem we've already proved.
for real problems with my statement, see your sibling comment.
Reward hacking will continue to be a problem. For sufficiently astonishing AI-created results, we must remember to ask if AI has not instead found it easier to elaborately fool us.
Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?
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.
And still that requires X to not be particularly large. It could conceivably be in ballpark of BB(40).
You, sir, have a very different definition of "not particularly large" than I do!
To be fair, BB(40) is smaller than almost all positive integers.
It’s practically zero, in fact.
This feels like saying there are probably hundreds of stars in the universe
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).
"A soundness bug in the Lean kernel (#14576) was reported and fixed during the week of July 27. [...] On July 25, Ramana Kumar published a repository containing a sorry-free "disproof" of the Collatz conjecture, produced with AI assistance. It is not a valid proof because it exploits a bug in the kernel's handling of nested inductive types. On July 28, Kiran Gopinathan reduced it to a small proof of False and opened issue #14576."
So essentially: One cannot trust the code produced by an LLM, even if the code is a formal proof passing the verifier.
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.