Remix clone Hacker News

new | show | ask | jobs Github

▲

amelius 3 hours ago

Not if it's lean-verified.

▲

bayindirh 3 hours ago | parent [-]

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

▲

Ethan_Barry 3 hours ago | parent | next [-]

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 3 hours ago \| parent [-]
		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.

▲

amelius 3 hours ago | parent | prev [-]

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

▲

bayindirh 3 hours ago | parent [-]

Yup, found it:

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

	▲	amelius 3 hours ago \| parent [-]
		Cool, thanks!