Terence Tao Rebuilds His 2018 Logic Textbook as a Lean-Powered Game
Lean Grimoire
Terence Tao has revived a 2018 JavaScript interactive textbook called QED, which teaches propositional and first-order logic as a crafting game, and rebuilt it with a coding agent under the working title "Lean Grimoire." The new version can display an in-progress Lean proof of the player's game state, and a fantasy mode turns statements into potions and expressions into scrolls. Tao is seeking playtesters to make it a better tool for teaching logic and Lean.
Just for fun, I also added an option to play in a "fantasy mode" in which various game elements are depicted using fantasy-themed flavor text.
- torben-friis
What a mess of an educational game.
Sorry to be so negative, but one can barely parse the LLMish introduction, and thosebcontrols seem like a half finished personal obsidian document.
Kind of weird coming from tao, I remember his math notes being quite approachable and well written.