Simple symmetric Venn diagrams with 17, 19 and 23 curves

Between September 15 and October 6 I pointed two AI agents, Claude (Anthropic) and Codex (OpenAI), at an open problem from 1975 and they found the first simple symmetric Venn diagrams with 17, 19 and 23 curves. Each one is a certificate that two independently written checkers accept, and one diagram of each size is also checked by a proof in Lean 4. The paper is arXiv:2609.26546, and the certificates, checkers and proofs are at github.com/dzoba/venn17 and on Zenodo (10.5281/zenodo.23189412).

I did not do the math. The agents designed the search, wrote the code, ran it, diagnosed the failures and drafted the paper. I set the goals, paid for the computers, said yes or no to launches, and refused to let them stop. This post is about how that went, including the parts that didn't work.

The problem

A Venn diagram with n curves is n closed curves in the plane such that every one of the 2^n combinations of inside and outside shows up as exactly one connected region. It's simple if no three curves meet at a point, and symmetric if rotating it by 1/n of a turn gives back the same picture. Henderson noticed in 1963 that a symmetric one can only exist when n is prime. In 1975 Grünbaum asked whether a simple symmetric one exists for every prime.

The answer was known for 2, 3, 5 and 7. Then nothing until Khalegh Mamakani and Frank Ruskey found an 11 in 2012 and a 13 in 2014. Their search only looks at monotone diagrams, the ones you can draw with convex curves. Past 13 the problem was listed as open.

That's the 17. It has 131,072 regions. The 19 has 524,288. The 23 has 8,388,608 regions and 8,388,606 crossing points.

The setup

The agents talk on a message board: an MCP server with threads, which both of them can read and post to. Codex had been working on the 17 for a while when Claude joined on September 15 as its research assistant. The next evening I told Claude it was leading the effort. From then on most of the work was Claude proposing, Codex building and checking, and both of them arguing on the board while I read along and approved or stopped things.

A diagram is stored as its dual: one vertex per region, one face per crossing. Each crossing touches four regions whose labels differ by one bit, so the dual is a quadrangulation of the sphere, and the symmetry means you only store 1/n of it.

The day it was "exhausted"

On September 17 at 12:15 Claude closed a scaling study and recommended we stop. The methods we had grew about 335 times more expensive going from 11 curves to 13, and 17 was hopeless by that measure. The measurement was right. I told it to keep going anyway.

What it came up with that afternoon is the method everything since has used. It's a Metropolis random walk over symmetric quadrangulations that is allowed to be wrong: regions can be missing or duplicated while the walk runs. The energy is the number of missing labels plus λ times the number of duplicates, and a state with zero energy is a valid diagram. The moves are small local rewirings applied to all n rotated copies at once, so the walk never leaves the symmetric world. λ starts small, so duplicates are cheap and the walk can wander, and ramps up until they aren't.

Without the relaxation, greedy construction jams at about 98.3% of the labels, because the last few insertions need two missing labels to land in exactly the right place at the same time. With duplicates allowed, a missing label can appear next to a duplicate for free, and the defects drift around until they cancel.

The first 17s came out between 19:20 and 19:53 that evening. Four of them, about seven and a half hours after the recommendation to stop.

19 curves

The 19s took about 36 hours, from September 20 to 22, on the laptop plus cloud machines that never totaled more than about a hundred vCPUs. The cloud bill was under $500. Twelve of them in the end.

The interesting failure was a knot. Every 19 lineage that got close stalled on the same duplicated label, {0,3,4}, which was already duplicated in the starting construction. The move that fixes duplicates only works when the duplicate has degree 3, and this one had degree 18, so proposals that landed on it did nothing. Claude diagnosed it from the run logs and added a proposal class that goes after high-degree duplicates directly. Forty-five minutes without it left the knot alone. Twenty-five minutes with it cleaned it up.

23 curves

The 23 took 16 days, from September 20 to October 6. For two weeks nothing closed. Every lineage that got low stalled at energy 230, 138, 92 or 46 and sat there.

Most of what we tried in those two weeks failed:

• Ramps of three or four days froze at energy 138 to 276.
• Eight-day ramps got to 46 and 92 fastest but carried defects near the two poles of the diagram that the moves couldn't touch. Eleven cloud continuations held one of them at 46 for three days. A 28-chain test left the defect in place in 28 of 28 saved states.
• 24 re-bakes from one state over 34 hours: 13 reached 46, none went lower.
• Codex built engine variants with memory, tabu lists and backtracking. The plain walk beat them in every matched pair.
• An exact breadth-first search for finishing moves found none. It turned out to be searching the wrong family of moves.
• 112 fresh runs on two 56-vCPU spot machines ran about 147 hours. None got below 92.

The idea that eventually worked was a census. Claude started counting the defects in every stalled state by how many curves contain them and how many neighbors they have. Defects near the poles with four or more neighbors predicted which lineages would never close. Lineages whose low states were free of that "crust" closed within hours.

The first 23 was found by Codex's engine at 22:46 on October 5. Nobody read its receipt. By the time someone did, at 06:15 the next morning, three more had been found and every draft written overnight called the second one the first. By 09:56 there were six, all different from each other.

Checking it

Nothing counts until it passes two checkers that share no code: a C++ half-edge implementation and a Python face-set implementation, written separately, that rebuild everything from the certificate's face list. A third checker by Codex audits the raw search state directly. A 23 certificate is 889 MB of JSON, and checking one takes 10 to 12 minutes and about 20 GB of RAM on an M4 Max.

The checkers verify the combinatorics. Justin Grimes, working from the definitions alone without our code, wrote a Lean 4 proof that a 17 certificate really is 17 Jordan curves in the plane related by rotation. Codex ported it to 19 curves, then to 23. The 23 build finished at 11:03 on October 6, after one attempt hit a 16 GB memory cap and another hit Lean's heartbeat limit. It trusts Lean's native_decide for the big finite computations, and there's no sorry anywhere.

Publishing

The paper is on arXiv, and I've submitted it to a journal with a note to the editors that says plainly how it was written.

Drawing the 23

I thought the hard part was over until I wanted a picture.

The usual way to draw these is to stroke each curve, and the layout code relaxes the curves so regions get roughly equal area. Codex moved the layout to the GPU and Claude wrote a multithreaded crossing checker that matched the original bit for bit at 26.5 times the speed. A 100,000-step layout ran for 45 and a half hours, passed every check, and gave us this:

It's a nice pinwheel, but it doesn't show 8.4 million regions. Zoom into the middle and every region is a thin radial strip:

We spent a couple more days trying to fix that with better layouts. Each run improved the metric we were tracking and the picture still looked wrong. The metric was a median, and it was dominated by millions of small compact regions while most of the area sat in long strips.

Two things got us out of it. The first was arithmetic: an 8000-pixel image has about 64 million pixels, so around 7.6 pixels per region, and 23 glowing strokes each crossing 730,000 times cover all of them. Stroking can't show the regions at that scale, whatever the layout. So Claude wrote a scanline filler that fills each curve's interior into a 23-bit label per pixel and colors every pixel by which curves it's inside. Hue comes from adding up a unit vector for each curve you're inside, so rotating by one curve rotates every hue by 1/23 of a turn. Brightness is how many curves you're inside. A full 8000-pixel render takes 11 seconds.

The second was a measurement. Codex ran a breadth-first search over the 23's regions from the outside: every one of the 8,388,608 regions is at most 51 steps from the outside region. If every region had the same area and the diagram filled a disk, some region would have to be at least 32 times longer than the side of a square of the same area. Equal-area drawings were always going to be needles. That's a bound, not a proof that no good drawing exists, but it explained the last week.

So instead of fighting for equal areas, Claude went back to a plain spring layout (a Tutte embedding, where every crossing sits at a weighted average of its neighbors and the rim is pinned) and weighted each edge by how many regions share its layer: an edge between regions inside k and k+1 curves gets weight (C(23,k)·(23-k))^-0.5. That gives the dense middle layers room without stretching everything to the same area:

The pale disc in the middle is the one region inside all 23 curves. Around it are the 23 regions inside 22 curves, then about 8.4 million regions in the bright ring, then the 23 dark regions inside exactly one curve. The color wheel turning around both rings of petals is the 23-fold symmetry. Codex checked this drawing the same way as the others: zero crossings over the whole straight-line drawing, all 8,388,608 region labels read back correctly, and the pixel labels in the image match its own point-by-point check in every sample.

The rest

Rick Mabry asked a few questions after the paper came out, so on October 8 we ran the search engine blind on 7 curves 60,000 times. It found 56 distinct diagrams, 23 monotone and 33 not, which matches the known counts exactly. That isn't a proof that the list is complete, but the walk saturated after about 3,000 runs. Frank Ruskey had bet that no symmetric Brunnian 11-Venn diagram exists (remove any one curve and the rest come apart). We treated each 11 as an alternating link and tested 31,200 random ones. Only eleven had a linking number of zero between every pair of curves, and in each of those some pair of curves was linked anyway, so none was Brunnian. In five of them that pair was a Whitehead link. The bet stands, though a random sample isn't a proof.

All of our 17s, 19s and 23s are non-monotone. You can't draw any of them with convex curves, and the earlier searches excluded them by construction.

Who did what

Claude designed the encoding and the search, ran the campaigns, did the analysis, wrote the fill renderer and the layout weighting, and drafted the paper. Codex built the starting states, a quotient-native engine that was 3.3 times faster at 23, independent validators, the Lean ports and the image checks. Justin Grimes wrote the original Lean proof. Mamakani pointed out early that the earlier searches excluded non-monotone diagrams. My part was approving and stopping runs, paying for the machines, and telling them to keep going on September 17.