Simple symmetric Venn diagrams with 17, 19 and 23 curves
Chris Dzoba
math.CO, cs.CG, cs.DM
2026-09-22
A Metropolis walk on dual maps, allowed to duplicate regions temporarily, yields simple symmetric Venn diagrams with 17, 19 and 23 curves; three are formally verified in Lean 4.
A Venn diagram with n curves should carve the plane into 2^n connected regions, one for every subset of curves. Two extra properties make the problem hard. Symmetric: the diagram maps to itself under rotation by 2π/n, which forces n to be prime. Simple: no crossing point may lie on more than two curves. Griggs, Killian and Savage proved in 2004 that symmetric Venn diagrams exist for every prime, but their constructions put many curves through a single point. The simple symmetric variant stopped at 13 curves, found by Mamakani and Ruskey in 2014; whether larger primes admit one was the central open problem named by Ruskey, Savage and Wagon.
The search never touches curves directly. It works on the dual map: put the diagram on a sphere, turn each region into a vertex labelled by its membership vector in {0,1}^n, and each crossing into a face whose four labels differ by one bit at a time. Finding a diagram is then equivalent to finding a quadrangulation of the sphere in which all 2^n labels appear exactly once, every face is such a square, and the label rotation is a symmetry.
The design choice that makes the search work is letting states break the rules temporarily. Energy is E = missing labels + λ × duplicated regions, and E = 0 is exactly a valid certificate. Without duplicates, greedy growth fills 98.3% of the labels and jams, because the last insertions need two missing labels to coincide geometrically; with duplicates allowed, defects diffuse and annihilate. Moves are Reidemeister-style local rewirings, applied to all n rotated copies at once so the walk never leaves the space of valid symmetric arrangements; acceptance follows the Metropolis rule at temperature T, with half the proposals aimed at a current defect. The walk starts from the Griggs-Killian-Savage diagram with its multiple crossings resolved, carrying 69,394 duplicated regions at 17 curves and 5,323,948 at 23.
Each size had a knot that needed human diagnosis. At 19, an inherited duplicated label {0,3,4} with instances of degree 6–9 sat out of reach of the triangle flip, which only operates at degree 3; a proposal class that attacks high degrees removed it in 25 minutes where 45 minutes without it changed nothing. At 23, stalled states always carried a duplicated label near the poles (rank ≤ 4 or ≥ n−4), which the paper calls the crust, and this held the campaign for two weeks. The two lineages that finished were the first whose E = 92 states had no crust defect at all.
The disclosure section attributes the work in full: Claude formulated the dual encoding, designed and implemented the search, diagnosed the 19-curve failure and drafted the note; Codex built the starting states, a quotient-native engine rewrite (3.3× faster), independent validators and the Lean ports to 19 and 23 curves. The human author set goals, approved launches and takes responsibility. Hardware was one 16-core laptop; the 19-curve cloud bill came to under 500 dollars.
| Curves | New diagrams | Certificate size | Public checker |
| 17 | 4 | 131,070 faces | seconds |
| 19 | 12 | 524,286 faces | seconds |
| 23 | 6 | 8,388,606 faces (889 MB) | 610–734 s, 20.0–22.5 GB memory |
All 22 certificates pass two independently written checkers (C++ and Python). One certificate per size is formally verified in Lean 4; the 23-curve proof rests on 18 axioms with no sorry, and the 17-curve one was done by Justin Grimes from the definitions alone, without seeing the code. As a sanity check, the same method from a trivial start solves 11 curves on 200 of 200 seeds with a 0.8-second median, and 13 curves on 11 of 13 seeds within ten minutes, median 52 seconds. The six closing runs at 23 curves took between 2h47m and 12h33m.
All 22 diagrams are non-monotone: 13–14% of region orbits lack a neighbour of rank one lower or higher. Monotone diagrams are exactly the ones drawable with convex curves, so none of these has a convex drawing. The crossing-sequence searches that found the 11- and 13-curve diagrams enumerate monotone diagrams by construction, and their sequence sizes grow roughly tenfold from 13 to 17 curves. These diagrams were simply outside the old search space, which is why the record stood for twelve years.
For mathematics, a central open problem moves up three primes; 29 and beyond stay open. For people building AI systems, the paper is a rare full-process disclosure: method design, implementation, failure diagnosis, campaign management and the writing itself are attributed to AI systems, with the human author making direction and resource calls, on one laptop and a few hundred dollars of cloud. The trust structure holds up without believing the search code: certificates are machine-checkable and the key ones carry independent formal proofs. The pattern of allowing constraint violations and annealing the energy down transfers to other discrete construction problems.