Comment by senderista

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