5 ms·

Not if it's lean-verified.

bayindirh 5d 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://x.com/gro_tsen/status/2082483878480977959 - https://infosec.exchange/@0xabad1dea/117002106099986943 https://infosec.exchange/@0xabad1dea/117002106099986943
- amelius 5d ago
  I don't know ... do you have a reference?
  - bayindirh 5d ago
    Yup, found it: https://news.ycombinator.com/item?id=49101465 https://news.ycombinator.com/item?id=49101465
    - amelius 5d ago
      Cool, thanks!
      - int_19h 5d ago
        You might also find this of interest: https://github.com/VladimirReshetnikov/Shenanigans https://github.com/VladimirReshetnikov/Shenanigans
- Ethan_Barry 5d ago
  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 5d ago
    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.
evenhash 5d 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 5d 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.
  - zahlman 3d ago
    Just because a proof is valid doesn't mean it proves the thing you want it to prove.
  - evenhash 4d ago
    What I’m saying is that you can’t just trust what the AI says because it produces a Lean artifact. The statement of the theorem has to be correctly translated from English into Lean code. It’s like translating user requirements into code. The code could run without bugs but not do what the users want. The only way to know the AI did it correctly is to check. You can’t just take it at face value.
- aureianimus 5d ago
  The thing is that there is a standard format where the definition of the theorem is split from the proof, and verifying that the definition matches the mathematical concept is a LOT less work then reading the proof, especially if you're willing to assume that definitions in Mathlib are correct.

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://x.com/gro_tsen/status/2082483878480977959 - https://infosec.exchange/@0xabad1dea/117002106099986943 https://infosec.exchange/@0xabad1dea/117002106099986943

amelius 5d ago
I don't know ... do you have a reference?
- bayindirh 5d ago
  Yup, found it: https://news.ycombinator.com/item?id=49101465 https://news.ycombinator.com/item?id=49101465
  - amelius 5d ago
    Cool, thanks!
    - int_19h 5d ago
      You might also find this of interest: https://github.com/VladimirReshetnikov/Shenanigans https://github.com/VladimirReshetnikov/Shenanigans
Ethan_Barry 5d ago
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 5d ago
  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.

evenhash 5d 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 5d 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.
- zahlman 3d ago
  Just because a proof is valid doesn't mean it proves the thing you want it to prove.
- evenhash 4d ago
  What I’m saying is that you can’t just trust what the AI says because it produces a Lean artifact. The statement of the theorem has to be correctly translated from English into Lean code. It’s like translating user requirements into code. The code could run without bugs but not do what the users want. The only way to know the AI did it correctly is to check. You can’t just take it at face value.
aureianimus 5d ago
The thing is that there is a standard format where the definition of the theorem is split from the proof, and verifying that the definition matches the mathematical concept is a LOT less work then reading the proof, especially if you're willing to assume that definitions in Mathlib are correct.