You don't know what you're talking about. Just because it was created by an LLM, and verified in Lean, does not make it true. The whole point of writing a proof is for it to be understandable.
Suppose I directed some llm agents to factor the primes from network logs of your machine. I then publish the private and public key in full. You would not change your keys of course because its not true right?
My argument is that LLM generation and a correlated Lean verification are not sufficient conditions. Both are falliable.
So is peer review. False proofs have been published before and will again. Does that mean journals are publishing slop?