To get the hang of this, I used Leanstral (Mistral’s LEAN agent) to vibe-code things like “the game of bridge” and then read the LEAN code.