Hacker News Reader

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

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

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.

I don't know ... do you have a reference?

Yup, found it:

https://news.ycombinator.com/item?id=49101465

Cool, thanks!

You might also find this of interest:

https://github.com/VladimirReshetnikov/Shenanigans

Reply on news.ycombinator.com