alt Hacker NewsDidn'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.
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.
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...