Remix.run Logo
▲ ijidak 3 hours ago

I think OP is saying Lean does indeed help.

▲kgwgk 16 minutes ago | parent [-]

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