| ▲ | bayindirh 3 hours ago | ||||||||||||||||
Didn't some of the recent proofs exploited a couple of blind spots of lean, and they were invalidated? Edit: Yup. A bug report to Lean was disguised as a "Collatz" proof in a humorous way. Links below. | |||||||||||||||||
| ▲ | Ethan_Barry 3 hours ago | parent | next [-] | ||||||||||||||||
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... | |||||||||||||||||
| |||||||||||||||||
| ▲ | amelius 3 hours ago | parent | prev [-] | ||||||||||||||||
I don't know ... do you have a reference? | |||||||||||||||||
| |||||||||||||||||