Educational Theorem Prover Game(Lean 4 Game)
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.
Worlds
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.
Raymond Smullyan's Knights and Knaves puzzles
Most of the puzzles in smullyan's book titled 'What is the name of this book' have been formalized and proven here
Run Locally, Make Your Own Game
Follow instructions at Game Skeleton to make your own game or to run this one locally.
Credits
This project was a collaboration between myself and @limb0007
Discussions on zulip made the dsl world for knights and knaves. Special thanks to @kbuzzard