# Lean Grimoire：用编码智能体重建逻辑教学游戏

> 原标题：Lean Grimoire

- 来源：Hacker News 首页
- 发布时间：2026-11-12T02:36:48.000Z
- AX AI 日报：https://ai-daily.ax0x.ai/items/xwkvk6mapt78gv91789itubo9
- 原文：https://terrytao.wordpress.com/2026/11/11/lean-grimoire/

## 摘要

作者用编码智能体重建了 2018 年的 Javascript 交互式逻辑教材“QED”，新版本暂定名“Lean Grimoire”，可展示当前游戏状态对应的 Lean 证明进度。应用还提供“fantasy mode”，把数学命题、表达式等元素替换为药水、卷轴等奇幻文本。作者希望获得试玩反馈，以提升其教授逻辑证明和 Lean 的效果。