A game is a fun interactive tutorial/puzzle/challenge that provides the user with a DAG of definitions, theorem statements, examples, etc. and asks the user to prove all the theorems in this DAG. For instance, there is the natural numbers game in Lean. Games are fun because of high interactivity, quick feedback, low entry barrier, ease of use, and absence of long boring reading. In this question, let's compile all the games available for all the proof assistants. Note: if some tutorial is highly interactive, accessible, etc. but its author doesn't call it a game, it can still be included here.
The max minigame
Short online game here. Something I knocked off with a couple of collaborators when we were trying to work out how to make a real number game. We still haven't got to the bottom of this.
Lean maze game
The Lean maze game. Me trying to work out how you can write bespoke tactics to do more than prove theorems. A short experiment.
The complex number game
The complex number game. You have to install Lean to play this one; It's an introduction to how to define the complex numbers from first principles in Lean (assuming anything you like about the real numbers) and prove they're a field.
A sokoban where your solution is a proof. You can play it in your browser thanks to the awesome work of Shachar Itzhaky (one of the jsCoq maintainers): https://coq-next.vercel.app/fun/coqoban.html