Lean Grimoire

Terence Tao has rebuilt an interactive textbook called "Lean Grimoire" that teaches propositional and first-order logic through a crafting game where players apply logical rules to solve problems. The modernized version, originally created in 2018 as "QED," now includes features like displaying Lean proofs in real-time and a "fantasy mode" that uses thematic language (such as calling statements "potions"). Tao is seeking playtesting feedback to improve the app as an educational tool for teaching logical proofs and the Lean proof assistant.