The following game offers a guided experience that teaches you the basics of proving theorems on a computer, specifically using the Lean theorem prover.
The final objective of the game is to teach you how to solve knights and knaves logic puzzles in a theorem prover. No pre-requisite knowledge regarding the puzzle or logic is needed, everything needed is slowly introduced in each world with plenty of hints and explanations.
The game is divided into the following worlds:
Equational Reasoning followed by Logic where there are three knights and knaves worlds you can choose from, each with its own approach to formalize and represent the logic puzzle.
Most of the puzzles in smullyan's book titled 'What is the name of this book' have been formalized and proven here
Follow instructions at Game Skeleton to make your own game or to run this one locally.
This project was a collaboration between myself and @limb0007
Discussions on zulip made the dsl world for knights and knaves. Special thanks to @kbuzzard