> 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.
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?
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 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?
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.
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.
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]
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.
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.
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.)
"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."
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.
Yeah people don't seem to get that the whole point of having a tightly checked kernel is so you don't have to care so much about the rest of it. Tactic heavy proofs have been "slop" long before LLMs got involved, and they lean heavily on the kernel rejecting nonsense.
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.
Mmm there are humans who think they make very few mistakes. Ones who actually make few mistakes, not sure about that one. Could be a mistake that they catch themselves very quickly, but I just don’t think humans are very good at generating 100% reliable output on the first try anywhere close to most of the time.
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.
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.
> Beware of bugs in the above code; I have only proved it correct, not tried it.
-Knuth, 1977
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?
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.
If AI is water, Lean is the pipe and collatz is a clog on one end, then surely we'll find the cracks.
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.
"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 ;)
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...
The proof was not actually a proof at all, because it was unsound (despite Lean admitting the proof).
(In practice, there’s also the possible error that the proved formal statement means something different than what you thought it meant.)
That said, I'm sure there's also room for underhanded Lean programming as well, which would be even more interesting.
Use Coq or Isabelle or any other decent theorem prover. Lean is just hyped.
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.
- Probably too close to corporations.
- Does not care about slop.
We have seen many projects that adopted AI under corporate pressure circle the drain. Often the corporations themselves backpedaled after some months.
Which?
> Often the corporations themselves backpedaled after some months.
Which
Mmm there are humans who think they make very few mistakes. Ones who actually make few mistakes, not sure about that one. Could be a mistake that they catch themselves very quickly, but I just don’t think humans are very good at generating 100% reliable output on the first try anywhere close to most of the time.