Simple symmetric Venn diagrams with 17, 19 and 23 curves
Chris Dzoba
math.CO, cs.CG, cs.DM
2026-09-22
允许区域暂时重复的 Metropolis 对偶图搜索,找到 17、19、23 条曲线的简单对称 Venn 图共 22 个,全部有机器可查证书,三个尺寸各一个经 Lean 4 形式化验证。
Venn 图要求 n 条闭曲线叠出的 2^n 种「在哪些曲线内部」的组合各对应一个连通区域。再加两条性质,问题立刻变难:对称,整图旋转 2π/n 后回到自身,这要求 n 是素数;简单,任何交叉点只许落在两条曲线上。Griggs、Killian、Savage 在 2004 年证明每个素数都存在对称 Venn 图,但那些图有多条曲线穿过同一点的交叉。简单又对称的版本,纪录停在 Mamakani 和 Ruskey 2014 年的 13 条曲线,更大的素数上是 Ruskey、Savage、Wagon 点名的中心公开问题。
搜索对象不是曲线,是曲线图的对偶图:图放到球面上,区域变顶点、配 {0,1}^n 标记,交叉变面,每个面的四个标记逐位翻转。找一张图等价于找一个 2^n 个标记各出现一次、每个面都是这类四边形、且在标记轮换下不变的球面四角化。
让搜索活下来的设计是允许暂时违规。能量 E = 缺失标记数 + λ × 重复区域数,归零当且仅当拿到合法证书。禁止重复时贪心构造填到 98.3% 就卡死;放开后缺陷能在图上扩散、相遇、湮灭。移动是 Reidemeister 式局部改接,每次同时施加到全部 n 个旋转像,保证游走始终不离开合法对称安排的空间;按 Metropolis 规则接受,一半提案瞄准现有缺陷。起点用 Griggs-Killian-Savage 图拆开多重交叉,自带大量重复(17 条 69,394 个,23 条 5,323,948 个),靠退火把能量压到零。
两个尺寸各有需要人肉诊断的死结。19 条:起点继承的重复标记 {0,3,4} 度数 6–9,而三角翻转只在度 3 区域起效,瞄准它的提案全部空转;补一类攻击高高度的提案,25 分钟消掉,不加则 45 分钟纹丝不动。23 条:卡死状态总在两极附近带着 rank ≤ 4 或 ≥ n−4 的重复标记,论文称为 crust,拖了两周;最终跑通的两条谱系,是第一批 E=92 状态里没有 crust 缺陷的。
论文按 Leiden 宣言逐项披露分工:Claude 提出对偶编码、设计并实现搜索、诊断 19 条的失败、起草全文;Codex 构造起始状态、写按旋转轨道存储的引擎改写(快 3.3 倍)、出独立校验器、把 Lean 证明移植到 19 和 23 条;人类作者定目标、管资源、对内容负责。硬件是一台 16 核笔记本,19 条阶段云开销不到 500 美元。
| 曲线数 | 新发现 | 证书规模 | 公共 checker |
| 17 | 4 个 | 131,070 面 | 秒级 |
| 19 | 12 个 | 524,286 面 | 秒级 |
| 23 | 6 个 | 8,388,606 面(889 MB) | 610–734 秒,20.0–22.5 GB 内存 |
22 张证书全部通过两个独立实现的 checker(C++ 与 Python)。17、19、23 各一张另做 Lean 4 形式化证明,23 条那份只依赖 18 条公理、无 sorry,17 条那份由第三方 Justin Grimes 不看代码独立完成。小尺寸自检:11 条曲线 200 个种子全部成功、中位 0.8 秒;13 条 13 个种子里 11 个十分钟内成功、中位 52 秒。收官六图各耗时 2 小时 47 分到 12 小时 33 分。
22 个图全部非单调,13–14% 的区域轨道缺一个 rank 恰差 1 的邻居;单调等价于可用全凸曲线绘制,所以它们都没有凸画法。当年找到 11、13 条的交叉序列搜索按构造只枚举单调图,序列规模从 13 到 17 条还要涨约十倍。新图根本不在旧方法的搜索空间里,这是纪录停滞十二年的直接解释。
数学侧,一个中心公开问题推进了三个素数,29 以上仍开放。AI 侧,这是一份少见的全流程披露:方法设计、实现、故障诊断、战役管理、写作都记在 AI 系统名下,人类作者做方向与资源决策,总成本是一台笔记本加数百美元云费。结果的可信结构也立得住,不要求读者相信搜索代码:证书机器可查,关键证书有独立形式化证明。允许违反约束、用能量最小化逐步收敛的搜索设计,可以搬到别的离散构造问题上。