Comment by bayindirh

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