Comment by senorcrab

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.