皮亚诺游戏 · Peano Game

把"写证明"变成"玩拼图"——免打字的可视化 Lean 4 自然数游戏。 用天平（rfl）、引理卡（rw）、归纳（induction）证明自然数的算术定理： 从 2 + 2 = 4 一路证到 add_comm、mul_add、mul_assoc。

• 每一步操作 1:1 映射一条合法 Lean tactic，右侧实时生成证明脚本
• 通关后证明可一键导出 .lean 文件
• 证出的定理变成金卡进入图鉴，后续关卡可用
• 移动优先、中英双语、亮/暗主题、纯静态部署

快速开始

npm install
npm run dev        # 本地开发 http://localhost:5173
npm test           # 全部测试（内核单测 + 属性测试 + 22 关参考题解重放 + UI 冒烟）
npm run build      # 构建 dist/
npm run preview    # 本地预览构建产物

架构

src/
  kernel/      证明内核（零依赖纯 TS，<700 行）
    term.ts      Term / Formula、解析、打印、语法相等（rfl 语义）
    match.ts     一阶模式匹配、出现位置枚举、替换
    tactics.ts   rfl / rw（含 ← 反向）/ induction、ProofState、tactic 日志、
                 参考题解重放引擎、Lean 导出
    lemmas.ts    内置引理卡表（NNG4 同款定义）
  levels/      关卡 DSL + 内容 + CI 校验
    levels.ts   22 关（教学 8 + 加法 5 + 乘法 9），每关带参考题解
    index.ts    解析、卡池合规校验、全量重放（verifyAll）
  game/        UI（React + zustand）
    store.ts    证明快照栈（撤销/重做）、进度/图鉴持久化（localStorage）
    components/ 天平、积木块、目标卡、手牌、卡池、脚本面板、选关、图鉴…
  kernel/*.test.ts     内核单测 + fast-check 属性测试
  levels/levels.test.ts 22 关重放 CI（npm test 硬门槛）
  game/smoke.test.tsx   UI 冒烟（jsdom）

设计要点

• rfl：目标两侧语法相等时天平转平发光，点「rfl 归位」关闭目标
• rw：点引理卡 → 真实一阶匹配 → 唯一匹配自动应用；多匹配高亮所有位置、点选具体位置（天然覆盖 nth_rewrite）；卡面 ↺ 翻面即 rw [← h]
• induction：点目标里的变量块 → 确认弹窗 → 目标分裂为「奠基 / 归纳步」两张目标卡，归纳步附带假设卡 hd（非归纳步目标激活时锁定置灰）
• 脚本面板：实时生成 Lean 证明，分支自动插入 -- base case / -- inductive step 注释；通关后导出 theorem … := by …
• 内核正确性：官方向题解逐关重放 + fast-check 属性测试 + 与 Lean 语法 1:1 映射的导出

关卡内容

22 关全部移植自 NNG4（leanprover-community/NNG4，Apache-2.0）：

• 教学世界（8 关）：rfl、rw、拆数字、反向改写、add_zero、精确改写、add_succ、Boss 2+2=4
• 加法世界（5 关）：zero_add（induction 初战）、succ_add、Boss add_comm、add_assoc、add_right_comm
• 乘法世界（9 关）：mul_one、zero_mul、succ_mul、Boss mul_comm、one_mul、two_mul、mul_add、add_mul、终极 Boss mul_assoc

署名

关卡设计移植自 NNG4（Kevin Buzzard 及 leanprover-community 团队），遵循 Apache-2.0 协议。

部署

纯静态站点：npm run build 后把 dist/ 部署到 Vercel / GitHub Pages 即可，进度保存在浏览器 localStorage，无后端。