Comment by Gehinnn
14 hours 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.
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.