> 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.
rzmmm 2 hours ago [-]
The implementation of the kernel is relatively trivial, it's an intentional design choice.
Cantinflas 57 minutes ago [-]
As claude would say, "relatively" is carrying a lot of weight in that frase. Definitely load-bearing — would not pass a quick smoke test.
sieabahlpark 2 hours ago [-]
[dead]
dafelst 1 hours ago [-]
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.
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?
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.
remywang 2 hours ago [-]
Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?
cperciva 2 hours ago [-]
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.
IsTom 2 hours ago [-]
And still that requires X to not be particularly large. It could conceivably be in ballpark of BB(40).
AnimalMuppet 1 hours ago [-]
You, sir, have a very different definition of "not particularly large" than I do!
Sharlin 41 minutes ago [-]
To be fair, BB(40) is smaller than almost all positive integers.
db48x 5 minutes ago [-]
It’s practically zero, in fact.
derdi 1 hours ago [-]
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.
paulddraper 57 minutes ago [-]
This had nothing to do with Collatz itself and everything to do with a Lean bug.
The proof was not a proof because it was not sound, even though Lean admitted the proof.
de_aztec 2 hours ago [-]
So essentially: One cannot trust the code produced by an LLM, even if the code is a formal proof passing the verifier.
layer8 2 hours ago [-]
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.)
fancy_pantser 2 hours ago [-]
One can only trust a verifier as far as they can trust anything made out of software.
AnimalMuppet 1 hours ago [-]
It has nothing to do with LLMs. One cannot trust the proof of anything if one cannot trust the verifier.
juhopitk 3 hours ago [-]
"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."
as1297 2 hours ago [-]
Lean has Claude contributions, what do you expect!
Use Coq or Isabelle or any other decent theorem prover. Lean is just hyped.
aseipp 2 hours ago [-]
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.
Jweb_Guru 1 hours ago [-]
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.
adw 2 hours ago [-]
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.
Zsfe510asG 2 hours ago [-]
There are humans who make very few mistakes. The presence of Claude in a project however tells you something about the attitude of the project:
- 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.
daishi55 14 minutes ago [-]
> There are humans who make very few mistakes
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.
muglug 2 hours ago [-]
> We have seen many projects that adopted AI under corporate pressure circle the drain.
Which?
> Often the corporations themselves backpedaled after some months.
Which
msdz 2 hours ago [-]
Why can’t your two criteria be applied to projects with human contributors without further due diligence?
josh-wrale 1 hours ago [-]
Claude can produce code that is professionally reviewed and found to be correct.
Ar-Curunir 2 hours ago [-]
Do you have any evidence that the bugs were due to LLM code? Or are you just speculating baselessly
Rendered at 21:26:46 GMT+0000 (Coordinated Universal Time) with Vercel.
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.
> 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?
If AI is water, Lean is the pipe and collatz is a clog on one end, then surely we'll find the cracks.
The proof was not a proof because it was not sound, even though Lean admitted the proof.
(In practice, there’s also the possible error that the proved formal statement means something different than what you thought it meant.)
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.
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.
Which?
> Often the corporations themselves backpedaled after some months.
Which