The other crucial part to this is the ability to actually encode and test the theorem (via Lean). Otherwise, we would be swarmed with a billion lines of theorems that no one will be able to ever understand and verify anyway.

If you think AI-generated Lean proofs are unreadable, imagine Opus 5 generating informal proofs.