Lean Grimoire

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 : 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. Share this: Print (Opens in new window) Print Email a link to a friend (Opens in new window) Email More Share on WhatsApp (Opens in new window) WhatsApp Share on Bluesky (Opens in new window) Bluesky Share on Nextdoor (Opens in new window) Nextdoor Share on Threads (Opens in new window) Threads Share on Tumblr (Opens in new window) Tumblr Share on Telegram (Opens in new window) Telegram Share on LinkedIn (Opens in new window) LinkedIn Share on X (Opens in new window) X Share on Facebook (Opens in new window) Facebook Share on Reddit (Opens in new window) Reddit Share on Mastodon (Opens in new window) Mastodon Share on Pinterest (Opens in new window) Pinterest