Lean Grimoire：用现代编程智能体重建的逻辑教学游戏

作者用现代编程智能体重建2018年JavaScript交互教材QED，并将项目命名为“Lean Grimoire”，以制作游戏教授命题逻辑与一阶逻辑。新版可展示游戏状态对应的进行中Lean证明，还提供以奇幻主题文本呈现数学元素的“fantasy mode”，作者希望获得试玩反馈以改进逻辑证明教学。