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.