Post

I'm learning to use Claude code for my Rocq proof development. First rule of fight club: If ANY proof attempt fails to compile, STOP IMMEDIATELY. Otherwise, Claude just exhausts my tokens.