| ▲ | Ethan_Barry 3 hours ago | |
There was a hash collision bug in the main Lean kernel that was patched, but AFAIK nothing relied on it. You'd have to know what you were doing to accidentally get there... | ||
| ▲ | bayindirh 3 hours ago | parent [-] | |
The incident in the links I posted exploited several bugs AFAICS, so it's a different story than a single hash collision bug, it seems. | ||