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…

Commenting on Bubbles has been removed. Why? If you want to talk about this post, write to the author, use the comments on their blog if it has them, or reply with a "RE:" post on your own blog. Suggestions? feedback@bubbles.town