陶哲轩用AI编程助手重制逻辑教学游戏Lean Grimoire
来源标题：Lean Grimoire
陶哲轩借助现代编程智能体重建了2018年的交互式逻辑教材《QED》，新版本暂定名为Lean Grimoire。游戏保留“制作类”玩法，让玩家通过应用逻辑规则从给定假设推出结论，并新增了显示当前游戏状态对应的Lean证明过程等功能。
以下正文由 AI 翻译自 Hacker News 最新（原文版权归原站所有），可能存在偏差，重要内容请以原文为准。
Terence Tao 关于研究、论述性论文、未解问题讨论及其他数学相关话题的更新。2026年11月11日，发表于 diversions, math.LO | 标签：applets, Lean | 作者：Terence Tao
早在七月，我就开始尝试用现代编程智能体来构建一些数学可视化小程序。由于过去几个月极为繁忙，我不得不把这些项目搁置一旁；但最近我抽出了一些时间，继续推进当时启动的一个项目——将我2018年制作的一个名为“QED”的 Javascript 互动教科书进行现代化改造，该书此前已在本博客上公布过。那本教科书的目的是以“制作游戏”的形式教授命题逻辑和一阶逻辑，玩家需要运用各种逻辑规则，从给定的一组假设中推导出目标结论。
借助编程智能体，我重建了这款游戏（暂定名为“Lean Grimoire”），并加入了许多新功能，例如可以选择显示当前游戏状态对应的 Lean 证明过程。纯粹为了好玩，我还添加了一个“幻想模式”选项，在该模式下，各种游戏元素会以奇幻风格的文本呈现（比如数学命题变成“药水”，数学表达式变成“卷轴”，等等）。下面是一张典型的截图，图中玩家已接近完成某个断言的证明：
我希望有人能对这款应用进行试玩测试，使其在教授逻辑证明和/或 Lean 方面更加实用。
正文由 探How 从来源站点 RSS 同步，内容未经改写；遇到排版缺失或需要图片、视频时请以原文为准。