Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Postmortem for Kernel Soundness Bug #14576

leodemoura.github.io

Post reply on HN
Print view View original

21–30 of 68 posts

Re: Postmortem for Kernel Soundness Bug #14576

#21

Post by muglug »

Zsfe510asG wrote: post #15
adw wrote: post #11

Earlier 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.

> We have seen many projects that adopted AI under corporate pressure circle the drain.

Which?

> Often the corporations themselves backpedaled after some months.

Which

Re: Postmortem for Kernel Soundness Bug #14576

#22

Post by derdi »

remywang wrote: post #6

Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?

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.

Re: Postmortem for Kernel Soundness Bug #14576

#23

Post by josh-wrale »

Zsfe510asG wrote: post #15
adw wrote: post #11

Earlier 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.

Claude can produce code that is professionally reviewed and found to be correct.

Re: Postmortem for Kernel Soundness Bug #14576

#24

Post by AnimalMuppet »

IsTom wrote: post #13
cperciva wrote: post #9

Earlier quoted context omitted.

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!

Re: Postmortem for Kernel Soundness Bug #14576

#25

Post by Jweb_Guru »

aseipp wrote: post #17
as1297 wrote: post #7

[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 (es…

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.

Re: Postmortem for Kernel Soundness Bug #14576

#28

Post by paulddraper »

remywang wrote: post #6

Isn’t a disproof of the Collatz conjecture easy to check as it should just be a counterexample? Or is the proof not constructive?

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).

Re: Postmortem for Kernel Soundness Bug #14576

#29

Post by Cantinflas »

rzmmm wrote: post #12
gr_norm wrote: post #5

> 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.

As claude would say, "relatively" is carrying a lot of weight in that frase. Definitely load-bearing — would not pass a quick smoke test.

Re: Postmortem for Kernel Soundness Bug #14576

#30

Post by Sharlin »

AnimalMuppet wrote: post #24
IsTom wrote: post #13

Earlier quoted context omitted.

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.
Post reply on HN