Lean Grimoire

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