Terence Tao released Lean Grimoire, a rebuilt version of his 2018 interactive logic textbook QED that teaches propositional and first-order logic through a crafting game and shows in-progress Lean proofs. Tao designed QED as a crafting game. Players apply rules of logic to reach a desired conclusion from a given set of hypotheses. The format teaches propositional and first-order logic through direct interaction with proofs.