The Harary–Hill and Zarankiewicz crossing-number formulas

The explanation

Put five dots on a page and join every pair with a line. That makes ten lines. Lines may curve, but however you route them, at least two must cross somewhere. One crossing is enough. With six dots and fifteen lines, the best drawing has three crossings. With seven dots it has nine. How does that number grow?

The guess has a precise form. Write n for the number of dots. Take n/2, (n−1)/2, (n−2)/2 and (n−3)/2, round each one down, multiply them, and divide by 4. For 5 dots that gives 2 × 2 × 1 × 1 / 4 = 1. For 11 dots it gives 100. Richard Guy published a drawing with this many crossings in 1960. In 1963, Frank Harary and Anthony Hill stated the conjecture: no drawing does better.

Drawings with that count were known. The hard part was the other direction. A drawing can route its lines in endless ways. Showing that nothing beats the formula means ruling out every one of them. Progress came in pieces. In 2007, Shengjun Pan and R. Bruce Richter used a computer to prove the formula for 11 dots, which gives exactly 100. Oswin Aichholzer reported a computer-assisted proof for 13 dots in 2021, giving 225. For large n, the best general bound reached more than 0.98559895 times the formula in 2019. Other proofs worked only when the drawing was restricted. One such rule puts every dot on one line and keeps each link to one side of it.

A second puzzle has the same shape. Paul Turán traced it to a brick factory near Budapest in 1944, with rail lines joining kilns to storage yards. In graph terms, every one of m dots on one side joins every one of n dots on the other. Casimir Zarankiewicz drew a layout with a matching formula, but his published proof that it was best had a gap. For three dots on each side, the formula gives one crossing. Daniel Kleitman proved the formula in 1970 when one side has at most six dots.

These two papers prove both formulas for every size, with any curved lines allowedSource 1,Source 2. The single difficulty, ruling out every drawing, is removed by turning a drawing into algebra. Each crossing gets a sign that records which way the lines pass. The paper also records the order in which lines leave each dot. For closed loops in the plane, these signed counts always cancel to zeroSource 3. That fact is turned into a statement about polynomials, formulas in several variables.

Take an odd number of dots. The paper builds a family of polynomials whose number of independent members is exactly the conjectured countSource 4. It shows that the crossings of a drawing carry enough information to pin down every member. A counting argument from linear algebra then shows the drawing needs at least that many crossings. Removing one dot handles even numbersSource 5. Known drawings show the count is reached.

The theorems count every crossing pointSource 6. If two lines cross three times, that is three crossings. Other ways of counting, such as counting each crossing pair of lines once, are different questions. Drawings that must use straight lines are also a separate question. The formula now holds for every number of dots, not only the cases computers could checkSource 1.

How sure is this? A computer proof checker called Lean has checked formal versions of both formulas, including drawings that reach them. Those formal versions count crossings as points, as the papers do. No specialist review of either paper has been published.

What it doesn't show. This does not settle the crossing numbers of drawings that must use straight lines.