陶哲轩用编码智能体重建逻辑教学游戏 Lean Grimoire

关于我的研究和说明性论文的更新、未解问题的讨论以及其他数学相关话题。作者：Terence Tao 2026年11月11日，发表于 diversions, math.LO | 标签：applets, Lean | 作者：Terence Tao 今年七月，我开始尝试使用现代编码智能体来构建一些数学可视化小程序。由于过去几个月事务极为繁忙，我不得不将这些项目搁置；但最近我抽出了一些时间，着手推进当时启动的一个项目——将我2018年制作的一款Javascript交互式教材“QED”进行现代化改造，该教材此前已在本博客上公告过。那本教材的目的是以“制作游戏”的形式教授命题逻辑和一阶逻辑，玩家需要运用各种逻辑规则，从给定的一组假设中推导出目标结论。 借助编码智能体，我重建了这款游戏（暂定名为“Lean Grimoire”），并加入了许多新功能，例如可以选择显示当前游戏状态的Lean证明进行过程。纯粹为了好玩，我还添加了一个“奇幻模式”选项，在该模式下，各种游戏元素会用奇幻主题的背景文字来呈现（例如，数学命题变成“药水”，数学表达式变成“卷轴”，等等）。下面是一张典型截图，其中玩家已接近完成该断言的证明： 我希望有人能对这款应用进行试玩测试，使其在教授逻辑证明和/或Lean方面更加实用。