The Harary–Hill conjecture: why 18 dots need 1,008 crossings

01The problem

Put some dots on a page and join every dot to every other dot with a line. The lines may bend as much as you like. How few times must they cross?

With four dots you can avoid crossings altogether. With five you cannot: however you draw it, at least one pair of lines crosses. Mathematicians call the picture with every dot joined to every other the complete graph K_n, and the smallest possible number of crossings its crossing number.

The numbers grow quickly. Eight dots need 18 crossings. For eighteen dots the answer was believed to be 1,008, but nobody could prove it. It is a question from graph theory, and one of the best-known unsolved problems about how graphs can be drawn.

02A formula nobody could prove

In the early 1960s Guy, Harary and Hill proposed a formula for the crossing number of complete graphs. It became known as the Harary–Hill conjecture, and sometimes as Hill's conjecture or Guy's conjecture:

Z(n) = ¼ ⌊n/2⌋ ⌊(n−1)/2⌋ ⌊(n−2)/2⌋ ⌊(n−3)/2⌋

The brackets mean "round down". For five dots the formula gives 1, for eight it gives 18, and for eighteen it gives 1,008.

Dots	5	6	7	8	9	10	11	12	18
Crossings	1	3	9	18	36	60	100	150	1,008

Classical drawings reach exactly this number, so the formula was always known to be achievable. What was missing was the other half: a proof that no cleverer drawing does better. For more than sixty years that had been shown only up to n = 12.

03What OpenAI claims

In a manuscript dated 23 September 2026, OpenAI reports a proof that the classical drawings are optimal for every n. If it holds, the formula stops being a conjecture and becomes the crossing number of every complete graph.

Resolves the Harary–Hill conjecture and Turán's brickyard problem in the Zarankiewicz formulation, determining the crossing numbers of every complete and complete bipartite graph. The result proves the optimality of the classical drawings among all plane drawings with continuous edge arcs.

A second manuscript makes the matching claim for complete bipartite graphs, where the dots come in two groups and lines only join dots from different groups. That question is known as Turán's brickyard problem, or the brick factory problem, and its expected answer as the Zarankiewicz crossing-number conjecture.

04What the animation shows

The Short builds the classical two-page drawing on a sphere, starting from five dots and one crossing and ending at eighteen dots and 1,008 crossings. Every gold dot is a real crossing in that drawing, and every chime you hear is one of them.

The animation illustrates the statement. It is not the proof, and it does not check it.

05Status and caveats

Preprint. The manuscripts have not been independently reviewed. Treat the result as OpenAI's claim until other mathematicians have checked it.

OpenAI's catalogue also links a Lean formalisation document for this result. We have not examined what that formalisation covers.

06Questions

Did AI solve the Harary–Hill conjecture?

OpenAI says the proof was produced by its AI. The manuscripts are public, but nobody independent has confirmed them yet.

Has the Harary–Hill conjecture been proved?

OpenAI reports a proof in a manuscript dated 23 September 2026. It has not yet been independently reviewed, so it is a claimed proof, not an accepted one. Before it, the conjecture was known to hold only up to n = 12.

What is the crossing number of K₁₈?

The Harary–Hill formula gives 1,008. Drawings with exactly 1,008 crossings exist; OpenAI's claim is that none has fewer.

Is this the same as the brickyard problem?

No, but they are siblings. The brickyard problem asks the same question when the dots come in two groups. OpenAI reports proofs of both.

07Sources

• The crossing number of complete graphsOpenAI preprint · 23 September 2026 · PDF
• The crossing number of complete bipartite graphsOpenAI preprint · 23 September 2026 · PDF
• OpenAI's public catalogue of maths results, result 165github.com/openai/math