Remix.run Logo
▲ kgwgk an hour ago

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