> Ultimately we think a fatal flaw was found in Mochizuki's proof, so it didn't lead anywhere in particular. But in our hypothetical "AI lean-verified proof of RH" situation, it would presumably generate substantially more of that community activity we saw in the Mochizuki situation. And if it's correct, that community activity would be productive (expository talks, students given problems to flesh out or generalize, etc).

This also sounds like a vector for trolling the community with complex putative proofs hiding a known flaw.

▲

amelius 3 hours ago | parent | next [-]

Not if it's lean-verified.

▲

bayindirh 2 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 2 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 2 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 2 hours ago | parent | prev [-]

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

▲

bayindirh 2 hours ago | parent [-]

Yup, found it:

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

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

▲

2 hours ago | parent | prev [-]

[deleted]