Comment by IsTom
8 hours ago
So that link(https://infosec.exchange/@0xabad1dea/117002106099986943) buried in the comments of comments sounds pretty damning.
8 hours ago
So that link(https://infosec.exchange/@0xabad1dea/117002106099986943) buried in the comments of comments sounds pretty damning.
https://lipn.info/@mevenlennonbertrand/116997927457012577 , you and they might be jumping to conclusions
My takeaway was not the involvement of the LLMs, which I consider to be irrelevant; the core was that there was an exploit of a flaw in the verification engine that allowed an incorrect proof to be validated. That is not great.
In addition to their use as tools for pure math, they are also used for software verification, where adversarial examples could have real-world applications in verifiable supply chain attacks.
Metamath (and specifically Metamath Zero) is formally verified.
Right, but the point is as far as I'm aware nobody accidentally found a bug in Lean by proving a theorem in a non adversarial context (and this submission is a link to a discussion at Mathoverflow). Also I think most formal verification is done using Coq and Isabelle/HOL, no?
2 replies →