*** 高级选读 · 交互式形式化证明入门
证明闯关
用四步完成一段证明：选择策略，观察目标怎样改变。
把条件、目标和每一步规则写清楚，再让网页检查。这就是本页的形式化证明体验，无需安装软件。
第1关：已知A → B和A → (B → C)，证明A → C。
A → B，A → (B → C) ⊢ A → C
本题规定：报名就有参赛卡；已报名的人，有参赛卡就可以参赛。
已知条件 · 你的卡牌
卡牌可以反复使用，使用后不会消失。
如果小林已报名，那么他有参赛卡。
如果小林已报名，那么只要他有参赛卡，就可以参赛。
当前目标 · 还需要证明什么
待证明
⊢ A → C
如果小林已报名，那么他可以参赛。
目标里的“如果”提示我们：先假设A，再证明C。
当前没有额外的临时假设。
选择策略
点击策略按钮，或者选择卡牌上的动作。
要证明“如果A，那么C”，可以先假设A，再证明C。
试着让所有已知条件为真，而目标为假。
证明步骤记录
- 还没有使用卡牌。
证明完成
把这段证明读成中文
前5关各有一条3—5步的参考走法，不限步数，可以撤销。分情况关和最后的反例挑战标为 **，可以以后再玩。选错时会解释原因，目标保持原样。完成记录只保存在当前浏览器。
先看懂，才知道下一步要做什么
目标变了，不等于原目标已经证明了
使用条件卡之前
已知 P，P → Q目标 ⊢ Q→
使用条件卡之后
已知 P，P → Q新目标 ⊢ P你可以顺着条件想：“有P，再用P→Q，就能得到Q。”也可以从目标倒着想：“我想得到Q；这张卡说只要有P就够了，所以先检查P。”网页用第二种方式展示目标变化。
hP : P 的意思是“名叫hP的这条已知条件说明P成立”。hP只是方便引用的名字。⊢ Q 在这个界面中标出当前待证明的Q；它不是一张已经拿到的卡牌。
A、B、C或者P、Q表示完整命题。第一关的A是“小林已报名”这句话，不是“小林”这个人。三角形关的P是“T是等边三角形”这句话，不是“等边三角形”这个对象。换一关时，页面会重新说明字母的含义。
本页用 → 表示命题中的“如果……那么……”。题目中的 A → B，A → (B → C) ⊢ A → C 读作：“以左边两条命题为前提，证明右边这条命题。”符号 ⊢ 分开前提与要证明的结论。
第一关为什么恰好可以走四步？
- 假设前件A。为证明A → C，临时假设A，目标变为C。
- 使用hABC，并用已有的A。A → (B → C)与A给出B → C。因此，要证明C，现在还需证明B。
- 使用hAB。A → B告诉我们，要证明B，只需证明A。
- 引用已有的A。A就在临时假设里，这个目标完成，整段证明随之完成。
第2步使用了A，第4步又使用了同一个A。假设没有被消耗。最后得到的是A → C，并不是无条件的C。
为什么不直接看图，说“它显然是等腰三角形”？
这里练的是从明确给出的前提得到结论。图形的含义帮助我们理解卡牌；网页检查的是推理结构。它不会自行判断一个实际图形是否等边，也不会替我们证明题目给出的前提。给前提本身提供依据，是另一个证明任务。
因此，同样的P、P→Q、目标Q，也可以解释成“n能被4整除”“如果n能被4整除，那么n是偶数”“n是偶数”。熟悉的例子换了，推理规则没有变。
每个动作，都对应一种明确的推理规则
怎样使用手里的卡牌
使用已有结论
已有：P
目标：P
目标和卡牌写的是同一个命题，可以直接完成。只写着Q的卡，不能被当作P。
使用条件
前提：P → Q；P
结论：Q
要证明Q时，先用条件卡，再完成P这个子目标。箭头不能随意倒过来。
证明“且”
目标：P ∧ Q
任务：分别证明 P、Q
两件都完成才算完成。反过来，已知P∧Q时，可以拆出P和Q。
证明“如果”
目标：P → Q
任务：假设 P，证明 Q
完成后得到的是“如果P，那么Q”；并没有无条件证明P是真的。
** 证明“或”
目标：P ∨ Q
任务：任选一边证明
证明P就足以说明“至少一个成立”，证明Q也可以。“或”允许两者同时成立。
** 使用“或”
已知：P ∨ Q
策略：分两种情况
若想得到R，要分别说明“假设P时能得R”和“假设Q时也能得R”。不能只完成较容易的一边。
数学里的卡牌不会被消耗。已经证明的结论可以反复引用；你也不必用完每一条已知条件。比喻的作用是帮助理解“手里有什么、还缺什么”。
** 网页怎样检查“不是乱点也能过关”？
每个动作都会建立一小段证明：记录所用前提、推理规则和子目标。全部子目标完成后，网页从最初的前提出发重新检查整棵证明树。只有最终结论与题目目标相同，才报告证明完成。
本页只实现上面几种命题逻辑规则。它是一个小型教学检查器，不是Lean 4，也没有声称实现完整的逻辑系统。最后的挑战另外检查真值反例；找到反例意味着前提不能保证目标，而不是目标已经被证明。
第一关的关键：证明一条“如果”
临时假设，只在对应的小证明里有效
第一关开始只有两张条件卡，没有A。目标是A → C，所以可以暂时假设A，在这个假设下证明C。完成后，整段证明给出A → C。
你证明的是“如果小林已报名，那么他可以参赛”。你没有证明小林已经报名，也没有证明他无条件可以参赛。虚线卡标出临时假设；小证明结束后，这张卡也结束它的作用。
** 分情况关的两个分支也各有自己的临时卡。假设P的分支只允许使用P这张新卡；假设Q的分支只允许使用Q那张新卡。两个分支都可以使用原来的前提，但不能混用对方的临时卡。两边都能得到同一个R，才能结束分情况证明。
** 这为什么和 Lean 一类证明助手相似？
证明助手通常把当前任务表示为“在这些条件下，证明这个目标”。一条指令可能用已有条件结束目标，也可能产生新的子目标，或者在局部加入假设。本页用中文按钮展示这些动作。
学习时先说清每个动作的意思，再接触实际工具中的命令，会更容易分清数学理由与输入语法。这里不要求记忆命令，也不把网页的显示当成Lean已经验证过的结果。
同一道题，在 Incredible Proof Machine 中怎样连线
推理已经正确，还能少用一个积木
你提供的截图是一段正确证明。若以这一关提供的基本积木数量最少为标准，可以把8块减到7块：去掉图中编号4的 ✎A 辅助标注块，直接重复使用同一个临时假设A。
在原图中怎样改：删除编号4的 ✎A 块，把编号8积木的A出口，直接接到编号5和编号6两块各自需要A的入口；其余连线保留。假设A仍然来自编号8的条件证明积木，并没有凭空增加一个前提。
七块怎么数？为什么已经最少？
两条给定前提占2块，目标占1块。推理需要4块：用A → B得到B；用A → (B → C)得到B → C；再由B → C和B得到C；最后通过条件证明积木得到A → C。合起来是2 + 4 + 1 = 7块。
在本题中，要从第二条前提取出C，需要连续两次使用条件；其中需要的B，要用第一条前提和A得到。外层还需要一次条件证明。这四个推理积木都各有作用。游戏的官方关卡配置也把本题的最少块数设为7。
这里比较的是本关给出的基本积木；把一段现成证明封装成自定义积木，不属于同一种计数标准。七块也不等于七个推理步骤：前提和目标本身都算积木。
对照：你提供的八块原图
辅助块只是把同一个命题输入后再输出，适合标注或明确中间结果；本题去掉它后，推理仍然完整。参见作者论文的第2.5节：辅助块。
给想继续探索的学生、家长与教师
推荐资料：继续玩证明游戏
- Incredible Proof Machine（推荐先试）：把推理步骤画成可连接的积木，连接已知条件与目标。它尤其接近“摆卡牌、接通推理”的想法。玩完本页后，可以从它的基础关卡开始，试着说出每一条连线所表达的推理。作者的ITP 2016论文第5节报告了13名、年龄13—20岁的学生参加工作坊的经验；多数学生事先没有相关逻辑或编程知识。这是小规模教学经验，不能直接推成适用于所有初中生的效果结论。
- Lean社区的学习入口推荐Natural Number Game，并链接提供逻辑、集合论等游戏的Lean Game Server。这些游戏使用真正的Lean，适合继续体验“写一步、看目标怎样变化”；仍需要适应工具语言和证明语法。
- Prooftoys的自然数游戏：通过选择表达式和菜单动作逐步构造证明。项目介绍以基础高中代数作为背景要求，可作为较少手写代码的另一种尝试。
针对初中低年级，本页采用较小的起点：完整命题P、Q；熟悉的偶数与三角形；少量规则；即时解释失败原因；随时撤销。能通关后，再请学生脱离按钮，用两三句话说明为什么成立。
本页是独立编写的教学练习，并未嵌入上述项目或复用它们的证明内核。推理动作在本地浏览器运行；外部工具和论文链接需要联网。