2 ms·
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 bu
by Gehinnn 2mo ago
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.
- 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.