This Lean game aims to provide an informal introduction to proofs and constructions in dependent type theory, aimed either at someone who is learning to write abstract mathematical proofs for the first time, or at a more experienced player who wishes to be reintroduced to proofs in a different formal system.

This game was originally created for a first year seminar course taught at Johns Hopkins University in Fall 2025 with the title "Computer-Verified Proof: a Hands-On Introduction to Interactive Theorem Proving." The original audience was comprised of a dozen students with a wide variety of academic interests, from economics to neuroscience.

Contributions to the game can be made by opening issues, submitting pull requests, or contacting me on the Lean zulip.

Acknowledgments: I am extremely grateful to the folks who built the Lean Game Server and the Game Skeleton Repository, as well as those who helped me solve a variety of problems that arose during the development of this game.