3 ms·
A correctness bug in a proof checker by definition means that you can prove false.
by markasoftware 2mo ago
A correctness bug in a proof checker by definition means that you can prove false.
- Smaug123 2mo agoNot 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.)
- markasoftware 2mo agogood point, I didn't think about these cases.
- Gehinnn 2mo agoBut 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.
- markasoftware 2mo agoLet 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.