结果族 187：Snaky in 21 Maker moves · 学科：Combinatorics · 验证状态：暂无形式化证明，请以社区核验为准
想象五子棋的亲戚：双方在方格纸上轮流占格，只有你（Maker）追求拼出一条固定的六格形状”Snaky”，对手（Breaker）专职堵你。此前人们只在”先手首回合下两子”的让子规则下会赢；这篇论文证明：不用任何让子，Maker 有一条 21 步内必胜的策略——悬置多年的平面无让子问题就此解决。
关键词卡片
看个具体例子
论文附上 728 张”必胜卡片”作为机器可查的证书（含校验和），并证明一条几何事实：当 Maker 手握一条四连、且对手在其邻域内至多占 3 格时，已胜或可强制取胜——这解释了一条四连为何压力巨大。251 格的固定落子区域与 17×17 棋盘上的同样结论一并给出。
为什么值得关心
一个具体博弈问题被彻底解决，其”数据证书 + 独立重构程序核验”的写法为计算机辅助证明提供了范式；步数与棋盘大小未必最优，强游戏（双方抢形状）也仍开放。
暂无形式化证明（AI 结果待核验）
第一级台阶
导读的”五子棋亲戚”落到纸面：棋盘是无穷方格纸，双方轮流各占一格、归属永久；只有一方（Maker）想拼出指定形状——六个方格连成的 Snaky，对手（Breaker）专职堵截。此前已知的赢法都要给 Maker 补偿（首回合下两子），论文要回答的是：分文不让，Maker 到底能不能赢。
第二级台阶
用本科语言精确化：这是 Maker–Breaker 游戏（弱游戏）：棋盘为整个格点集，目标 S = {(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)}，其允许拷贝为 t + R(S)，其中 t 是整平移、R 取八个带符号坐标置换矩阵（旋转、反射皆可，不许缩放）。让子（handicap）指给 Maker 的额外补偿；必胜策略指对 Breaker 一切合法续着都保证取胜的完整方案。
第三级台阶
| 定理在这样的语境下陈述：初始空棋盘、Maker 先行、无任何让子——这正是 Sieben 2008 年记录为悬而未决的平面无让子问题；此前 Halupczok–Schlage-Puchta 只证得三维必胜、8×8 棋盘必败、让子至多一。结论（定理 1）：存在单一的全局合法 Maker 策略，无论 Breaker 如何应对，至多 21 次实际落子即完成一个允许拷贝（对应交替博弈第 41 个单步回合）；且全部落子可限制在固定的 251 格区域内，17×17 棋盘上同样成立。证明路线是”条件必胜位置”三元组（要求集 A、信封 T、高度 h）配合组合规则递归合并，终点是一张 A 为空、 | T | = 251、h = 21 的证书卡，其正确性规则在文内数学证明、数据由独立程序核验。论文不声称步数或棋盘最优，强游戏仍开放。 |
在无限空棋盘上的 Snaky 六格骨牌 Maker–Breaker 游戏中，先手 Maker 有一条固定策略，无论 Breaker 如何应对，都能在自己的第 21 步落子之内拼出 Snaky 的允许拷贝；同一界在 @@M@@17\times17@@ 棋盘上也成立。这解决了悬置多年的平面无让子问题。
多格骨牌达成游戏（polyomino achievement game）由 Frank Harary 提出：双方在棋盘上轮流各占一格，只有 Maker 追求拼出指定形状，对手 Breaker 专职阻挠，这就是弱游戏（weak game，即 Maker–Breaker 游戏）。目标 Snaky 是六格骨牌 @@M@@S=\{(0,0),(1,0),(2,0),(3,0),(3,1),(4,1)\}@@。此前进展多依赖”让子”：Halupczok 与 Schlage-Puchta 证明 Snaky 在三维必胜、在 @@M@@8\times8@@ 棋盘上（对 Maker）必败、平面让子数（handicap number）至多为 1——即 Maker 首回合下两子才有已知必胜构造；Ito 与 Miyagawa 亦给出让子一的构造。Sieben 在 2008 年明确指出：无让子的普通平面问题当时悬而未决。本文正面解决这一问题，并给出 21、25、35 步三套完整构造。
主定理：存在单一的全局合法 Maker 策略（policy），对抗 Breaker 的一切合法续着，在实际落子至多 21 次内完成 @@M@@S@@ 的一个允许拷贝（allowed copy）——即 @@M@@t+R(S)@@，其中 @@M@@t\in\mathbb{Z}^2@@，@@M@@R@@ 取八个带符号坐标置换矩阵（平移、旋转、反射皆可，不许缩放）。这对应交替博弈中至多第 41 个单步回合取胜。推论给出有限棋盘版：同样的 21 步界在初始为空的 251 格棋盘 @@M@@T_{727}@@ 及 @@M@@17\times17@@ 棋盘 @@M@@\{0,\ldots,16\}^2@@ 上成立——事实上 Maker 可把全部落子限制在固定区域 @@M@@T_{727}\subseteq\{0,\ldots,16\}^2@@ 内。作者不声称步数或棋盘尺寸最优，也不处理双方都抢形状的强游戏（strong game）。论文还独立证明一个几何命题：若轮到 Maker 时它拥有四连 @@M@@\{(0,0),(1,0),(2,0),(3,0)\}@@，且 Breaker 在邻域 @@M@@Q=([-3,6]\times[-4,4])\cap\mathbb{Z}^2@@ 内至多占 3 格，则 Maker 已胜或可强制取胜——这解释了为什么一条四连能施加巨大压力。
核心工具是”条件必胜位置”，论文称为 valid claim：三元组 @@M@@(A,T,h)@@，其中 @@M@@A@@ 是要求集（Maker 须已拥有），@@M@@T@@ 是信封（envelope，不得含任何 Breaker 子），@@M@@h@@ 是高度（还需 Maker 落子数的上界）。只要局面满足 @@M@@A\subseteq M@@ 且 @@M@@B\cap T=\varnothing@@，Maker 便已赢或能在 @@M@@h@@ 步内赢。关键在于该定义对额外 Maker 子与 @@M@@T@@ 之外的 Breaker 子毫无限制，故天然覆盖无限棋盘上任意远处落子，无需棋盘截断或分情形讨论。
先建立六个”基”：@@M@@(S\setminus\{s_j\},S,1)@@——已占某拷贝的五格，补最后一格即胜。再反复用组合规则（combination rule）递归合并：给定若干有效 claim 与枢轴（pivot）@@M@@p@@，令 @@M@@T=\{p\}\cup\bigcup_iT_i@@、@@M@@A=(\bigcup_iA_i\cup\bigcap_iT_i)\setminus\{p\}@@、@@M@@h=1+\max_ih_i@@。正确性骨架是：Maker 占下 @@M@@p@@（若 @@M@@p@@ 已归它则任占一空格，照实计一步）后，各孩子要求集与信封交集 @@M@@\bigcap_iT_i@@ 都归 Maker；于是 Breaker 的一步回应不可能落进每个 @@M@@T_i@@，必有一个孩子既避开新回应、又（由 @@M@@T_i\subseteq T@@）避开全部旧 Breaker 子，沿它递归，高度严格递减。
证书本体是 728 张编号”卡片”：六个基加上第 6 至 727 行共 722 行数据，每行写明枢轴与孩子列表，全部用 18 字符字母表编码的精确整数坐标和向后引用表达。终卡 727 有 32 个孩子、按六个卡号分组摆放，每组放置后的要求集恰为 @@M@@\{(8,8)\}@@，且表中逐组把信封交集中的剩余格数削减到 0，故全部信封交集恰为 @@M@@\{(8,8)\}@@，于是 @@M@@A_{727}=\varnothing@@、@@M@@|T_{727}|=251@@、@@M@@h_{727}=21@@：空棋盘上前提自动成立。最后把递归证明转成单一先验策略：预先固定 @@M@@\mathbb{Z}^2@@ 的枚举与孩子的打印顺序，每轮占当前枢轴（若已被自己占用则占枚举中首个空格），Breaker 回应后选打印顺序中第一个信封避开该回应的孩子；高度从 21 降到基的 1，至多 21 步收尾。四连命题的证明则先做五连分叉（fork），再对行端点做垂直攻击（perpendicular attack），按三类旧阻挡子情形穷举，该部分技术细节较多，此处从略。
验证分三层：规则的博弈论可靠性（组合规则与六个基以引理形式在文内数学证明）、数据生成的精确集合（两套独立实现的重构程序核查全部 1,620 个组合节点与 37,042 个局部回应类，并附 SHA-256 校验和）、发布文件同一性。主结果未经 Lean 形式化——论文明言所附 Python 重构不自身确立任何 Lean 定理或内核编译；同族的 25 步、35 步姊妹构造沿用同一组合规则独立复现同一结论，互为佐证。按 OpenAI 官方声明，未经形式化的结果可能有问题，请以社区核验为准。
问 1：整个证明最脆弱的一环在哪里？
| （答：在数学规则与数据的接口处。组合规则与六个基的可靠性以引理形式在文内证明，这部分短而可人查；但 728 张卡片上 1,620 个组合节点与 37,042 个局部回应类的精确整数坐标、向后引用是否严格满足规则，只能机器核验。终卡本身是纯算术恒等式：32 个孩子按六组摆放后信封交集恰为 {(8,8)}、A 为空、 | T | = 251、h = 21——一个下标抄错即全盘皆输，好在这一层有两套独立实现的重构程序加 SHA-256 校验和兜底。） |
问 2：条件必胜位置 (A, T, h) 的设计为什么能免掉棋盘截断？
（答：该定义对”Maker 额外占格”与”T 之外的 Breaker 占格”毫无限制，只要求 A ⊆ M 且 B ∩ T = ∅。于是 Breaker 在无穷远处落子根本不破坏前提，证明天然覆盖无限棋盘，无需截断或分情形——这与此前 QBF 编码类工作只处理有限棋盘形成本质区别。）
问 3：21 步是最优的吗？8×8 必败与 251 格必胜矛盾吗？
（答：不矛盾也不最优。论文明确不声称步数或棋盘尺寸最优；Halupczok–Schlage-Puchta 的 8×8 必败说明胜负对棋盘敏感，而本文的 251 格区域嵌在 17×17 内（289 格），恰在必败的 8×8 与无穷棋盘之间。真正的最优步数问题论文未展开。）
问 4：与已有工作相比真正新意是什么？
（答：此前平面无让子问题悬置多年，已知构造都要让子一（首回合两子）；本文首次给出无让子必胜，且方法上把 Sieben 的证明树改造成”Maker 回合处陈述”的条件位置（枢轴已占时另有 Breaker 回合推论），显式追踪任意历史占格并计算实际落子数。四连压力也被提炼成独立几何命题：Maker 拥有四连且 Breaker 在邻域至多 3 格即已胜或可强制取胜。）
问 5：这类 AI 生成证明最可能出什么错？
（答：恰是”证书式证明”的软肋——规则与数据两张皮。规则证明正确、数据核验通过，仍可能因核验程序对规格的共同误读而双双失守（两套实现若同源则独立性存疑）。论文自己承认：所附 Python 重构不确立任何 Lean 定理、不经内核编译；25 步、35 步姊妹构造用同一组合规则独立复现结论，可作部分佐证但非形式化担保。）
问 6：谁会用到它，剩下什么？
（答：多格骨牌达成游戏社区——它了结了 Snaky 的平面无让子问题，并把”数据证书 + 独立重构核验”立为计算机辅助证明的一个可复制范式。仍开放：强游戏（双方抢形状）、最优步数与最小棋盘、其余十几种六格骨牌的无让子判定。）
总评
（一个小而干净的悬置问题被彻底解决，证明结构把人类可查的短规则与机器可查的长数据分离得当，可信度设计在同批论文中相当出色；最大风险只剩核验程序的独立性与规格误读这一条窄缝。）