AI 中文总结
本文通过Metropolis游走构造了17条和19条曲线的简单旋转对称维恩图，并提供了机器可验证的证书及Lean 4形式化证明，解决了此前仅知13条曲线的问题。
AI 中文摘要
我们展示了具有17条曲线和19条曲线的简单、旋转对称的维恩图：n条Jordan曲线通过旋转2π/n相互转换，且2^n个区域全部存在并连通；由于这些图是简单的，每个交叉点恰好位于两条曲线上。对称维恩图对于每个素数数量的曲线都存在（Griggs, Killian和Savage, 2004），但那些图有许多曲线通过同一点；简单的图此前仅已知最多13条曲线（Mamakani和Ruskey, 2014）。通过在一个旋转不变的球面四边形剖分上进行Metropolis游走，从Griggs-Killian-Savage图（其多重交叉点已解决）出发，找到了四个17曲线图和九个19曲线图，其中区域可能暂时重复。每个图都附带一个机器可检查的证书；每种规模的一个证书已通过Lean 4中的形式化证明验证。所有图都是非单调的，这就是为什么找到11曲线和13曲线图的交叉序列搜索无法找到它们的原因。
英文摘要
We exhibit simple, rotationally symmetric Venn diagrams with 17 curves, with 19 curves and with 23 curves: $n$ Jordan curves carried to one another by rotation through $2π/n$, with every one of the $2^n$ regions present and connected and, since the diagrams are simple, every crossing on exactly two curves. Symmetric Venn diagrams exist for every prime number of curves (Griggs, Killian and Savage, 2004), but those diagrams have many curves through a point; simple ones were known only up to 13 curves (Mamakani and Ruskey, 2014). Four 17-curve, nine 19-curve and five 23-curve diagrams were found by a Metropolis walk on rotation-invariant quadrangulations of the sphere in which regions may temporarily be duplicated, started from the Griggs-Killian-Savage diagram with its multiple crossings resolved. At 23 curves the walk was held for two weeks by duplicated regions near the poles; the two lineages that finished were the first whose $E=92$ states had none. Every diagram is given by a machine-checkable certificate; one certificate each of the 17- and 19-curve sizes has been verified by a formal proof in Lean 4. All of the diagrams are non-monotone, which is why the crossing-sequence searches that found the 11- and 13-curve diagrams could not have found them.
Comments14 pages, 2 figures. Certificates, independent checker, Lean 4 verifications and search code are archived at doi:10.5281/zenodo.22885649 and at https://github.com/dzoba/venn17. v2: five simple symmetric 23-curve diagrams added (found 5 and 6 October 2026); title changed accordingly
