Lean 4 with Mathlib proofs formally verify one 17-curve and one 19-curve Venn diagram certificate as simple rotationally symmetric Venn diagrams, using native_decide.
Abstract
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, twelve 19-curve and six 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-, 19- and 23-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.
Problem
Simple rotationally symmetric n-Venn diagrams exist only for prime n. They were previously known only up to n = 13. Their existence for 17, 19 and 23 curves was open.
Approach
Each diagram is encoded as its dual map, a quadrangulation of the sphere whose vertices carry n-bit labels and whose faces are cube squares. A Metropolis walk searches rotation-invariant quadrangulations, temporarily allowing duplicated regions. It starts from the Griggs–Killian–Savage diagram with its multiple crossings resolved. Resulting certificates are checked by independent C++ and Python checkers. One 17-curve certificate was formally verified in Lean 4 with Mathlib by Justin Grimes, and that development was ported to 19 curves by Codex.
Figure 2: The 17-curve diagram c178d7bd unrolled: its seventeen congruent sectors, each a fundamental domain of the rotation containing 131{,}070/17=7{,}710 crossings, drawn as rows, with the colour of each curve advancing by one position from row to row. The whole diagram is one row bent around the centre seventeen times.
Results
Simple symmetric Venn diagrams with 17, 19 and 23 curves were found, and all are non-monotone, so they lie outside the search space of earlier methods. Lean proofs completed for one 17-curve and one 19-curve certificate; the 23-curve Lean build passed the finite checks but had not finished when this version was prepared.
Figure 1: One of the nine 19-curve diagrams (certificate fcb7ad34 ), drawn from its certificate at near-uniform crossing density by the plotter described in the data repository: 19 curves, 524{,}286 crossings, every one of the 524{,}288 regions present exactly once. The centre hole is the region inside all 19 curves; the outer face is the region outside all of them. Colours identify curves.
