证明：电脑（Maker）在 21 步内必胜

先玩游戏 · 下载证书

本游戏中电脑的走法不是搜索或启发式，而是逐字执行论文《Snaky in 21 Maker moves》（OpenAI, 2026-09-25）中的 21 步证书（data/certificate.txt，SHA-256 3fa12d36…3d04）。下面给出完整的证明链，以及每一环对应的机器检查。

1. 游戏

无限平面 ℤ²，初始为空。Maker（电脑）先手，双方轮流各占一个空格，占有是永久的。Maker 只要占满任意一个 Snaky 副本即获胜：

S = {(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)}      □□□■■
允许的副本 = t + R(S)，R 为 8 个有符号置换矩阵   ■■■■□

Breaker（你）不需要拼出自己的形状，只需阻止 Maker。

2. 条件获胜局面（"卡片"）

定义。 三元组 (A, T, h)，A ⊆ T 为有限集，h ≥ 1。称其有效：只要轮到 Maker 走、且

A ⊆ M（Maker 已拥有 A），
B ∩ T = ∅（Breaker 在 T 中没有子），

则 Maker 已经获胜，或能在至多 h 步内获胜。注意这里不限制 Maker 在别处多出的子，也不限制 Breaker 在 T 之外的子。

有效性在任意平移、旋转、镜像 F 下保持（F 把策略整体搬过去），所以卡片可以"放置"后复用。

基础卡（引理 2）。 对 Snaky 的每个格子 s_j，(S∖{s_j}, S, 1) 有效：若 s_j 已是 Maker 的，S 已完成；否则 s_j 是空的（Breaker 不在 S 中），下它即胜。

组合规则（引理 1）。 设 (A_i, T_i, h_i)（i = 1..r）有效，p 为一格。令

T = {p} ∪ ⋃ T_i
A = ( ⋃ A_i  ∪  ⋂ T_i ) ∖ {p}
h = 1 + max h_i

则 (A, T, h) 有效。

证明。 设轮到 Maker、A ⊆ M、B ∩ T = ∅。因为 p ∈ T，Breaker 不拥有 p。Maker 下 p（若 p 已是自己的，就下任意空格——这也计为真实的一步）。此后 Maker 拥有 ⋃A_i ∪ ⋂T_i。若已获胜则停止。否则 Breaker 下某格 b；b 不是 Maker 的，所以 b ∉ ⋂T_i，于是存在 i 使 b ∉ T_i。由于 T_i ⊆ T，之前的 Breaker 子也不在 T_i 中。于是 A_i ⊆ M 且 B ∩ T_i = ∅，子卡 i 的前提成立，Maker 再用至多 h_i 步获胜，总计 ≤ 1 + h_i ≤ h。∎

关键：Breaker 一手棋只能占一个格子，而所有子包络的交集已经归 Maker，所以不可能同时破坏所有子卡。Breaker 在 T 之外落子则不影响任何子卡。

3. 证书

证书一共 722 行（卡 6..727），每行是组合规则的一次（嵌套）应用，引用的都是编号更小的卡。由结构归纳，728 张卡全部有效。对最终卡：

p₇₂₇ = (8,8),  A₇₂₇ = ∅,  |T₇₂₇| = 251,  h₇₂₇ = 21

A₇₂₇ = ∅、空棋盘上 B = ∅，所以前提在开局时成立，Maker 至多 21 步获胜。∎

4. 从证明到程序（`snaky.js`）

策略与论文 §"One strategy against every continuation" 一致：

当前活动声明 = (组合节点, 全局放置 F)。开局为 (卡 727, 恒等)。
Maker 下 F(p)；若已被自己占据，则下固定枚举中的第一个空格（替代步，照常计数）。
Breaker 应手 b 之后，按证书中的顺序选第一个 F(T_i) 不含 b 的子；引用子的放置为 F∘G。
到达基础卡时补上缺失的一格，获胜。

每走一步高度严格减 1，从 21 开始，所以至多 21 步。界面上的"AI 保证 ≤ k"就是已走步数 + 当前卡高度 − 1，它在整局里不会增大。

5. 机器检查

检查	命令	结果
论文自带短校验器	`python3 -B verification/verify_certificate.py`（在论文目录）	`PASS`
论文完整重建套件（21/25/35 步三套证书）	`python3.13 -B verification/supporting/verify_all.py --output-dir …`	`PASS`
本项目独立证明检查器	`python3 -B proof/check_proof.py`	`PASS`
浏览器引擎对抗测试	`jsc tests/run_tests.js -- 2000`	`PASS`，10000 局

`proof/check_proof.py`（独立实现）

它不调用论文的代码，自己解析、求值证书，并在 全部 1620 个组合节点 上直接检查一步博弈需要的局部条件。设 M₀ = A ∪ {p}（Maker 下完枢轴后至少拥有的集合）：

L1 每个 A_i ⊆ M₀ —— 子卡的必需集已到手
L2 每个 T_i ⊆ T —— 旧的 Breaker 子仍在子包络外
L3 h ≥ 1 + h_i —— 高度下降
L4 对 T ∖ M₀ 中每个可能的 Breaker 应手 b，存在 i 使 b ∉ T_i（T 之外的应手选 i = 0）
L5 p ∈ T —— Breaker 不可能已占据枢轴

再检查 6 张基础卡确实是"Snaky 缺一格"，以及最终卡 A = ∅、h = 21、T ⊆ {0..16}²。最后从空棋盘出发，遍历策略实际可达的全部 (节点, 放置) 状态，计算 Breaker 任意应对下所需的最多 Maker 步数。

[1] 证书求值: 728 张卡, 1620 个组合节点, 4089 个引用
[2] 局部条件 L1-L5 在全部 1620 个组合节点成立, 共检查 35422 个 (节点, Breaker 应手格) 对
[3] 6 张基础卡均为 "Snaky 缺一格", 高度 1
[4] 最终卡 727: A = ∅, |T| = 251 ⊆ {0..16}², h = 21
[5] 从空棋盘可达的不同策略状态 (节点, 放置) 数: 53823; 最坏情况所需 Maker 步数 = 21
PASS: Maker 在任何 Breaker 应对下都能在 21 ≤ 21 步内完成 Snaky

35422 个 T 内应手加上每个节点 1 个"T 外"应手类（1620 个），合计 37,042，与论文 §verification 报告的局部应手类数一致。

L1–L5 正是第 2 节组合规则证明里用到的全部事实，所以这一检查加上那段证明，就覆盖了 Breaker 在无限棋盘上的任意应手（T 外的应手等价于一个类）。Maker 多出来的子只会减少 Breaker 的合法选择，不会破坏任何条件。

`tests/run_tests.js`（检查真正跑在浏览器里的代码）

它用 macOS 自带的 JavaScriptCore 加载与网页同一份 snaky.js 和 certificate.js，先核对论文表格中的数值，再让 5 种 Breaker 各下 2000 局。每个 Maker 回合都断言不变量 A ⊆ M、B ∩ T = ∅，以及"已走 + 剩余高度 ≤ 21"。

Breaker	说明	最多 Maker 步数
random	在棋盘附近随机落子	8
envelope	只在当前包络 T 内随机落子	9
worst	每步选择让 Maker 进入剩余高度最大的子卡（即证书意义下的最强防守）	21（2000 局全部恰为 21）
greedy	封堵被最多"活"Snaky 副本覆盖的格子	8
mixed	每步随机换一种策略	12

结论：上界 21 是紧的（对这个策略而言）——最强防守能把电脑拖到第 21 步，但拖不到第 22 步。

6. 说明

这里证明的是"这个策略 21 步内必胜"，不是"21 是 Maker 的最优步数"（论文也没有这样声称）。
网页显示的是 23×23 的窗口；规则上棋盘是无限的。窗口外的落子对 Maker 没有影响（T₇₂₇ ⊆ {0..16}²，图中用虚线框标出）。