← Back to context

Comment by zahlman

7 hours ago

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

10 comments

zahlman

Reply
amelius  7 hours ago

Not if it's lean-verified.

  • evenhash  3 hours ago

    "Lean-verified" is not some magical incantation that makes a supposed proof irrefutable. Even disregarding potential bugs in the kernel as others have said.

    Say that AI gives you a Lean proof and says it proves Theorem X. It could just as easily give you the same proof but claim that it proves (not X). How would you know the difference?

    Nothing can really be considered proven unless a human expert can read the Lean proof and determine that (X as defined in the Lean proof) corresponds to X. The proof (at least the statement of the theorem) must be intelligible to humans to have value.

    It's possible people will just start taking AI at its word. Maybe AI says "Here is a Lean proof of X" and we all just shrug and go "Okay, X is proven." But that's not how it works right now for human mathematicians. Why would we apply that standard for AI?

    • tmhn2  1 hour ago

      I'm not totally sure what you mean. You can validate the proof using lean, which is what it's for--the whole magic of it is you don't have to just trust what AI says. That said, to your larger point, there are loopholes, and we'd certainly better be able to read the statement in lean, etc.

  • bayindirh  6 hours ago

    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