4 ms·

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 "Coll

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://x.com/gro_tsen/status/2082483878480977959 - https://infosec.exchange/@0xabad1dea/117002106099986943 https://infosec.exchange/@0xabad1dea/117002106099986943

amelius 5d ago
I don't know ... do you have a reference?
- bayindirh 5d ago
  Yup, found it: https://news.ycombinator.com/item?id=49101465 https://news.ycombinator.com/item?id=49101465
  - amelius 5d ago
    Cool, thanks!
    - int_19h 5d ago
      You might also find this of interest: https://github.com/VladimirReshetnikov/Shenanigans https://github.com/VladimirReshetnikov/Shenanigans
Ethan_Barry 5d 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 5d 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.