[flagged]
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.
Postmortem for Kernel Soundness Bug #14576
11–20 of 68 posts
Re: Postmortem for Kernel Soundness Bug #14576
#12> 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 guarant…
The implementation of the kernel is relatively trivial, it's an intentional design choice.
Re: Postmortem for Kernel Soundness Bug #14576
#13Isn’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).
Re: Postmortem for Kernel Soundness Bug #14576
#14> 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 guarant…
The implementation of the kernel is relatively trivial, it's an intentional design choice.
[dead]
Re: Postmortem for Kernel Soundness Bug #14576
#15[flagged]
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.
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.
Re: Postmortem for Kernel Soundness Bug #14576
#16So 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.)
Re: Postmortem for Kernel Soundness Bug #14576
#17[flagged]
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.
Re: Postmortem for Kernel Soundness Bug #14576
#18Reminds 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?
Re: Postmortem for Kernel Soundness Bug #14576
#19Earlier quoted context omitted.
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.
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.
Why can’t your two criteria be applied to projects with human contributors without further due diligence?
Re: Postmortem for Kernel Soundness Bug #14576
#20Reminds 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…
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