Terence Tao Rebuilds QED Logic Game as Lean Grimoire With a Coding Agent

What happened

Mathematician Terence Tao has released a rebuilt version of an interactive logic textbook, now carrying the working title Lean Grimoire, and is asking for playtesters. In a November 11 post on his blog, which reached Hacker News's front page the following day, Tao says he rebuilt the project with the help of a modern coding agent and added features intended to make it useful for teaching logical proofs and for learning the Lean proof assistant.

From QED to Lean Grimoire

The app is a modernization of QED, a JavaScript interactive textbook Tao originally built in 2018 and announced on his blog at the time. QED taught propositional and first-order logic in the form of a crafting game: starting from a given set of hypotheses, the player applies rules of logic until arriving at a target conclusion.

Tao writes that he began experimenting with coding agents to build mathematical visualization applets back in July, but that a hectic few months forced him to set those projects aside. He recently found time to return to one of them, and the rebuilt game is the result.

What the rebuild adds

Two additions stand out. The first is an option to display an in-progress Lean proof of the player's current game state, so that moves made in the game correspond to steps in a proof a proof assistant can track. The second is a lighthearted fantasy mode that decorates the game with fantasy-themed flavor text, in which mathematical statements appear as potions and mathematical expressions as scrolls.

The post does not name which coding agent Tao used or quantify how much of the implementation it handled, only that the rebuild was carried out with one.

An open call for playtesters

Tao closes the post by asking readers to playtest the app, with the stated goal of making it more useful as a means of teaching logical proofs and Lean. The Hacker News placement puts that request in front of a large audience of technical users, the group most likely to both stress-test the game and give meaningful feedback on the Lean integration.

Why it matters

Lean Grimoire is a modest project, but it sits at the intersection of three current threads.

It is a concrete, named example of a research mathematician using agentic coding tools to ship working software. Tao frames the agent as the thing that let him revive an eight-year-old side project he otherwise lacked bandwidth for, which is precisely the dormant-but-valuable work these tools are argued to unlock.

It also attempts to bridge two audiences: people learning formal logic through a game, and people learning Lean, a proof assistant with a growing role in mathematical formalization. Showing the Lean proof alongside the game state gives learners a visible path from intuitive rule application toward machine-checked proof, rather than treating the proof assistant as a separate, steeper skill.

Finally, the community reaction is part of the story. A front-page Hacker News appearance is how niche tools like this find testers and contributors, and Tao is explicitly asking for both.