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

早在七月，我就开始尝试使用现代编码代理来构建一些数学可视化小程序。由于过去几个月极为繁忙的事件，我不得不把这些项目搁置一旁；但最近我找到了一点时间，来处理当时启动的一个项目，即把我2018年制作的Javascript 交互式教科书现代化，该书名为“QED”，并曾在本博客上宣布过。那本教科书的目的是以“制作游戏”的形式教授命题逻辑和一阶逻辑，玩家应用各种逻辑规则，从给定的一组假设中得出期望的结论。

借助编码代理，我重建了这款游戏（我给它起的暂定名为“Lean Grimoire”），并加入了许多新功能，例如可以选择显示当前游戏状态的 Lean 证明进度。纯粹为了好玩，我还添加了一个“幻想模式”选项，其中各种游戏元素都用奇幻主题的文本描述（例如，数学命题变成“药水”，数学表达式变成“卷轴”，等等）。下面是一张典型的截图，其中玩家几乎完成了在给定 的情况下对断言 的证明：

我希望有人能对这个应用进行一些试玩测试，使其作为教授逻辑证明和/或 Lean 的工具更有用。