Hacker News Reader

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.

Reply on news.ycombinator.com