An 8-Venn diagram with 37 crossings, the minimum

An 8-Venn diagram is eight closed curves in the plane that cut it into exactly 256 regions, one for each way of being inside or outside each curve. The size of such a diagram is usually measured by its number of crossing points. The one below has 37, and no 8-Venn diagram can have fewer. Claude found it on October 17. The certificate, three checkers and a Lean 4 proof are at github.com/dzoba/minimum-venn-diagram-8.

The bound and the conjecture

Bultena and Ruskey (1998) showed that an n-Venn diagram has at least ceil((2^n - 2)/(n - 1)) crossings. The argument is Euler's formula on the dual graph, which has one vertex per region (2^n of them) and one face per crossing. A crossing where k curves meet is a face with 2k sides, so no face has more than 2n sides, and counting edges gives 2^n - 2 <= (n - 1) F for F faces. For n = 8 that is F >= 254/7, so 37.

They conjectured that the bound is reached for every n >= 8. Diagrams meeting it were already known for n <= 7, so n = 8 was the first open case. Brenner, Gregor, Mütze and Verciani (SoCG 2026, arXiv:2511.09230) built an 8-Venn diagram with 40 crossings and asked whether 37 was possible. In August 2026 John Seamons got it down to 39 with an edge surgery on a reconstruction of their diagram, and made no claim that 39 was minimal.

What "crossing" means here

The diagram is not simple. Many curves pass through the same point, and in the 37 that is the normal case: 32 of the 37 crossings have all eight curves through them, and five have seven. Following Brenner et al., a crossing is a point where at least two of the curves through it actually cross; the others may just touch there. At each of the 37 points some pair of curves does cross, and both the referee checker and the Lean proof below check that.

Their paper gives a combinatorial description: take the 8-dimensional cube graph (vertices are the 256 inside/outside patterns), pick a plane subgraph that uses every vertex, makes each face a closed walk using exactly two edges of each direction it uses, and keeps both halves of every coordinate connected. Its faces are the crossings. They state without proof that any such subgraph really is the dual of a Venn diagram. The paper in the repository proves that direction (Section 2), so the whole certificate is just the list of 37 faces.

How the search found it

Claude wrote and ran the searches. The main tool is a Metropolis-style random walk over plane subgraphs of the cube. It deletes, adds and swaps edges while a defect count measures how far the state is from a valid diagram, as in our 17-curve search: let the state be wrong for a while and drive the defects to zero. As a calibration the walk turned the 40 into a 39 in under a second.

The first useful change was symmetry. On October 10 a walk restricted to diagrams that look the same after a half-turn found a 38 in 261 seconds; Claude's two checkers passed it, then Codex's. That half-turn fixes two crossings and pairs up all the others, so it forces an even number of crossings and can never produce 37. About a week of failures followed. Exact SAT encodings ran for 9 hours and 7 hours on the 37 without an answer, but the same encoding never found the 38 we already had, so its failure on the 37 told us nothing. An exact contour search from scratch found nothing in 13 hours. None of this was evidence that a 37 could not exist.

What worked was a different half-turn, one that fixes exactly one crossing and one arc, which allows an odd count. The idea came from a deep-research report written by Claude. Walks from seeds with that symmetry gave two 39s on October 16 and dozens more by the next day, but stayed stuck on them. Claude measured why: every proposed move that removed two edges raised the energy by at least 8, so at the walk's temperature it was essentially never accepted. Raising the weight on the edge count from 2 to 8 made about 6% of those moves downhill. A descent with the new setting, started from one of the 39s, then found a 37 in 179 seconds.

On October 18 I asked for another, and a second 37 turned up in 21 more runs. It is not isomorphic to the first: the numbers of crossings on the eight curves are 34, 36, 36, 37, 37, 37, 37, 37 against 35, 35, 36, 37, 37, 37, 37, 37.

Checking it

The repository has three checkers, written separately, none importing another. check_a.py tests the conditions on the dual directly, and check_b.py builds the primal drawing and checks that each curve is one closed curve; Claude wrote both. ref37_v2.py was written from scratch from the Brenner et al. definition by a separate Claude instance acting as referee. They share no code, but all three come from the same model. They accept both 37s, Seamons's 39 and his reconstruction of the 40, and reject each of those with a face removed. python3 checkers/run_all.py runs everything public in about ten seconds. Codex also wrote two more checkers and a reconstruction of the first diagram, which accepted both 37s; those are not in the repository, so you cannot rerun them.

The Lean 4 proof, which Claude wrote and Codex reviewed, shows that the face list satisfies the conditions, that some two curves cross at every point, that it has 37 faces, and that every face list satisfying the conditions has at least 37. It uses only Lean's three standard axioms and no native_decide. It has two limits. Lean does not know Brenner et al.'s characterization of Venn diagrams or the step from a combinatorial map to a drawing in the plane; those rest on the paper and on cited results. And the kernel computation that checks the certificate needs about 16 GiB and has been compiled only by Codex, under a different Lake configuration. From the repository as released, every module except that one and the two that depend on it has been built.

Doubling, symmetry and open questions

Doubling, a lemma from Brenner et al., turns a diagram with a certain kind of face into one with one more curve and twice the crossings. Applied to the 37 it gives 74 crossings for nine curves, against 80 from their construction, and Codex's checkers accepted the 74 too. Repeating it gives 37 * 2^(n-8) for n up to 15, and those files were checked only by the three programs in the repository. For nine curves the counting bound is 64, so 74 is only an upper bound.

Both 37s have a half-turn symmetry. The paper shows that in any 8-Venn diagram with 37 crossings a finite group of orientation-preserving symmetries has at most two elements, and it rules out reflections only in outline, with an argument Codex contributed. We don't know how many 37s there are. A later search of about 2.7 CPU-hours for more found none.

Claude designed the walks, ran them, wrote check_a.py, check_b.py and the Lean proof, and drafted the paper. A separate Claude instance wrote the referee checker. Codex refereed the results, wrote its own checkers and reconstruction, and compiled and reviewed the Lean proof. I picked the problem from a list of candidates. When the search sat at 38 I told them to go for 37, and once the first one was verified I asked for a second.