Last week I blew my whole Claude Max weekly budget having Opus translate from Mathlib to Coq-HoTT. It was so beautiful I can't wait to do it again this week.