Lean Grimoire：用编码智能体重制逻辑教学游戏，可展示 Lean 证明进度

Back in July, I started experimenting with using modern coding agents to build a number of mathematical visualization applets. With the extremely hectic events of the last few months, I had to set those projects aside; but I recently found a bit of time to work on one such project that I had started back then, which was to modernize a Javascript interactive textbook I had made back in 2018, entitled “QED”, and announced previously on this blog. The purpose of that textbook was to teach propositional and first-order logic in the form of a “crafting game”, where one applied various rules of logic to reach a desired conclusion from a given set of hypotheses.

With a coding agent, I rebuilt the game (which I have given the working title of “Lean Grimoire”) with a number of new features, for instance giving the option to show an in-progress Lean proof of one’s game state. 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 (for instance, mathematical statements become “potions”, mathematical expressions become “scrolls”, and so forth). Here is a typical screenshot, in which one has nearly completed the proof of the assertion given :

I would be interested in having some playtesting of this app to make it more useful as a means to teach logical proofs and/or Lean.