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?

"true" != "understandable"