undefined

points

[-]

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.

by HappyPanacea4 hours ago|

parent|

[-]

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?

by Diogenesian4 hours ago|

parent|

[-]

But I think this has to be judged against an adversarial influx of LLM-assisted pseudomathematics slop vendors. A sorry-free proof in Lean (or Rocq!) whose top-level types check out is not good enough. You gotta check for compiler chicanery in all the private methods.

Or, alternatively: refuse to accept a Lean program as a valid proof. I assume LLMs are pretty good at Lean -> mathematical English in LaTeX.

by seanhunter3 hours ago|

parent|

[-]

This is something that people have thought about a fair bit and that link does not mean what you think it means

https://lean-lang.org/doc/reference/latest/ValidatingProofs/

Lean's threat model is not that it's designed so you can just take random lean code at face value without even reviewing it or whatever. It's designed to be a proof assistant to help working mathematicians validate proofs and not validate an "honest" incorrect proof. Malicious proofs that have been specifically constructed to exploit the proof system are known to be a possibility and are considered to be bugs that people try to fix, but they are not cause for serious concern.