Lean 魔典
内容提要
陶哲轩用编码智能体重建了2018年的逻辑教学游戏“QED”，新版本暂名“Lean Grimoire”，新增显示当前游戏状态的Lean证明进度，并加入奇幻主题模式（如命题变“药水”、表达式变“卷轴”）。他希望玩家试玩，以改进其逻辑证明与Lean教学效果。
延伸解读
从QED到Lean Grimoire：教学工具的现代化
陶哲轩2018年制作的逻辑教学游戏“QED”以“合成游戏”形式教授命题逻辑和一阶逻辑，玩家需应用逻辑规则从假设推出结论。新版“Lean Grimoire”借助编码智能体重建，保留了核心玩法，但加入了显示当前游戏状态的Lean证明进度功能。这一改动将游戏过程与形式化证明工具直接关联，使玩家在游戏中的每一步都能对应到Lean中的证明状态，有助于理解逻辑规则在证明助手里的实际表示。
奇幻模式：降低学习门槛的趣味包装
新增的“奇幻模式”用奇幻主题文本替换游戏元素，例如数学命题变为“药水”、数学表达式变为“卷轴”。这种包装不改变底层逻辑规则，但通过叙事化外观降低初学者的陌生感，让抽象符号更易接受。陶哲轩将其定位为“just for fun”，说明该模式主要服务于趣味性，而非教学严谨性。读者可将其视为一种吸引玩家投入的辅助手段，而非核心教学创新。
试玩反馈是改进教学效果的关键
陶哲轩明确表示希望有人试玩这个应用，以改进其作为逻辑证明和Lean教学工具的效果。这表明当前版本仍处于开发阶段，功能与教学流程尚未定型。对于潜在玩家或教育者而言，参与试玩并提供反馈，能直接影响工具后续的优化方向。文章未提及具体反馈渠道或版本发布时间，因此关注重点应放在试玩体验本身，而非期待一个已完成的正式产品。
Q&A
Lean Grimoire 是什么？
Lean Grimoire 是陶哲轩用编码智能体重建的逻辑教学游戏，原名“QED”，旨在通过游戏方式教授命题逻辑和一阶逻辑。
Lean Grimoire 相比原版 QED 有哪些新功能？
新增了显示当前游戏状态的 Lean 证明进度，以及一个奇幻主题模式，其中数学命题变为“药水”，数学表达式变为“卷轴”等。
陶哲轩为什么开发 Lean Grimoire？
目的是让玩家通过试玩来改进其逻辑证明与 Lean 教学效果，使应用更有用于教授逻辑证明和/或 Lean。
Lean Grimoire 中的奇幻模式是什么样的？
奇幻模式用奇幻主题的文本描述游戏元素，例如数学语句变成“药水”，数学表达式变成“卷轴”等。
如何参与 Lean Grimoire 的测试或提供反馈？
陶哲轩希望有兴趣的人试玩该应用，以帮助改进其作为逻辑证明和 Lean 教学工具的效果。
Lean Grimoire 的教学目标是什么？
教授命题逻辑和一阶逻辑，通过“ crafting game”形式应用逻辑规则从假设推导结论，并辅助学习 Lean 证明。
