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?

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.