Lean Grimoire

Lean Grimoire is an interactive game for learning propositional and first-order logic by constructing proofs. It modernizes QED, a JavaScript “crafting game” created in 2018, in which players apply logical rules to a set of hypotheses to derive a target conclusion. The example proof task is to establish that A implies the conjunction of A and B, illustrating how the game turns formal reasoning into a sequence of hands-on moves.

The updated version was rebuilt with help from a modern coding agent and adds the option to display the corresponding Lean proof as the player works. This connects the game’s visual, rule-based interface to a proof assistant used to formalize mathematics, potentially making it useful both for teaching logic and for introducing Lean. A fantasy mode gives mathematical objects playful names: statements become potions and expressions become scrolls. The project is still being developed, and its creator is inviting players to test it and help assess how well it teaches logical proof and Lean.