← Back to context

Comment by bayindirh

9 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.

- https://x.com/gro_tsen/status/2082483878480977959

- https://infosec.exchange/@0xabad1dea/117002106099986943

5 comments

bayindirh

Reply
Ethan_Barry  8 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  8 hours ago

    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.