I keep hearing about these insane fuck-ups in Lean. Surely checking definitional equality in some circumstances by comparing hashes alone (let alone a weak 32-bit hash) is gross negligence? What's wrong with Lean's technical direction? Are the maintainers inexperienced?
JP Aumasson
@veorq
Aug 12
proof of 0 = 1 in Lean, exploiting a hash collision (weak 32-bit hash Expr.hash/mixhash) github.com/endrazine/lean-cv…

Aug 13, 2026 · 8:55 AM UTC

1
62
34,641
Sort replies: Relevant Recent Liked
Replying to @barrowfaustus
this is not what is happening - the check for hash equality is just a quick early return on negative cases for definitional equality the bug is the exact same one that was fixed in v4.32.2
edu sandalo@eduardosandalia
Aug 13
Replying to @veorq
this is the same bug that was fixed recently the hash is just a quick check for equality, if they do collide, Lean does the full definitional check the reason this worked for previous versions is that it is exploiting the bug that some nested inductive types were skipped
36
2,034