In a talk called "A reintroduction to proofs" emilyriehl.github.io/files/reintr... I've speculated about teaching an undergraduate level introduction to proofs course but using dependent type theory as the implicit formal system in place of set theory and first order logic.

This past fall, I taught a first year seminar course at Johns Hopkins along these lines. As part of the course, I developed the Reintroduction to Proofs Game: adam.math.hhu.de#/g/emilyrieh... which is now featured on the Lean Game Server: adam.math.hhu.de

The game uses Lean tactics to animate the analogy between function types and implications, product types and conjunctions and so on.

Following a suggestion made by Kevin Buzzard this past summer, there is a world studying constructions involving the empty type before introducing negations, which allows us to separate out constructive proofs (eg double negation introduction) from classical ones (like double negation elimination).

The prefix "re" the title imagines more experienced players who might like to learn more about dependent type theory, the Curry Howard correspondence, or constructive mathematics.

This game was made possible by the good folks who built the Lean Game Skeleton repository and answered questions on the Lean for teaching thread on the Lean zulipchat, such as Alex Kontorovich, Aaron Liu, and Dan Velleman.