logoalt Hacker News

senderista • yesterday at 11:45 PM • 1 reply • view on HN

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

Replies

ijidak • yesterday at 11:47 PM

I think OP is saying Lean does indeed help.

➕ show 2 replies