Every vertex sits on one line and every edge is a half-circle above it or below it. Two edges cross exactly when they are on the same side and their ends alternate along the line. The paper's rule puts edge ij above when (i + j) mod n < ⌊n/2⌋. Tap an edge to flip it, scramble to start from chaos, and descend to flip greedily until no single flip helps. You will not get below Hill's number. For drawings of this shape, that has been a theorem since 2013. The 2026 claim is that no drawing of any shape does better.
Every kiln needs a rail line to every yard, and every crossing of two lines is where trucks jump the rails. Zarankiewicz put the kilns on a horizontal axis and the yards on a vertical one, each split as evenly as possible across the middle. Drag any kiln or yard to try a better layout. The count is exact: the coordinates are compared with integer-safe orientation tests.
This is the strongest check a browser can make. It tries every way to split Kₙ's edges between the two sides of the line and asks whether any split has fewer crossings than Hill's number. It's a branch-and-bound search: a partial split is abandoned as soon as the crossings it must already have reach the target. It runs in a background thread.
| n | Hill | nodes | time | anything below? |
|---|
What a "no" means: no two-page drawing beats Hill's number for that n. Ábrego, Aichholzer, Fernández-Merchant, Ramos and Salazar proved that for every n in 2013. The 2026 claim covers every drawing at all, with curves routed however you like. A finite search cannot reach that, which is why the proof is a proof. crossing.selftest.mjs runs this search for every n up to 11 on each change.
| n | Hill's number | status before 2026 |
|---|
The lower bound for every n was open. The best general results were ratios: at least 0.83 of Hill's number for large n (de Klerk et al., 2006), raised to more than 0.9855 (Balogh, Lidický and Salazar, 2019).
Complete bipartite graphs. Kleitman (1970) settled every K_m,n with one side of at most 6. Woodall (1993) settled K₇,₇ and K₇,₉ by computer. The best balanced bound was cr(K_n,n) ≥ 0.9118·dₙ² + o(n⁴) (Balogh et al., 2023).
Pál Turán was doing forced labour at a brick factory near Budapest. Small trucks ran on rails from every kiln to every storage yard, and wherever two rail lines crossed, the trucks tended to jump the track. How should the lines be laid out to cross as little as possible? With m kilns and n yards this asks for the crossing number of the complete bipartite graph K_m,n.
Kazimierz Zarankiewicz drew the layout in the draw tab and published a proof that it was optimal, ⌊m/2⌋⌊(m−1)/2⌋⌊n/2⌋⌊(n−1)/2⌋ crossings, but the proof had a gap. The companion question for the complete graph Kₙ, every point joined to every other, came from Guy, Harary and Hill around 1960. It is Hill's formula: ¼⌊n/2⌋⌊(n−1)/2⌋⌊(n−2)/2⌋⌊(n−3)/2⌋. Matching drawings were found early. Proving that nothing does better stalled at small cases and asymptotic fractions for sixty years.
Two papers dated 23 September 2026, written by an internal OpenAI model and released on 6 October as part of a collection of 722, claim to finish both problems. One proves Hill's formula for every n. The other proves Zarankiewicz's formula for every m and n. Both are for all drawings: any curves, any vertex positions, with every crossing point counted.
Both main theorems are formalized in Lean. The release ships each one's statement as a short, separate file that a checker called Comparator compares the proof against, using only Lean's three standard axioms. The statement for Kₙ is 89 lines and defines everything from scratch: drawings as continuous paths in ℝ², crossings that are finite and transversal with no triple points, and the crossing number as the minimum over all such drawings. Its last lines are:
def hill (order : ℕ) : ℕ :=
(order / 2 * ((order - 1) / 2) * ((order - 2) / 2)
* ((order - 3) / 2)) / 4
theorem complete_graph_crossing_number (order : ℕ)
(at_least_three : 3 ≤ order) :
ordinaryCrossingNumber (completeGraph order) = hill order
This page's formulas are written exactly as those definitions are, floor division and all. We did not run the Lean check ourselves. It means building a 26-million-line library, which is the release's job and is reproducible from its repository. The papers are preprints, and the release itself says some of its results "could have issues". A formal statement narrows that a lot but does not remove the need for human reading.
crossing.js is the only copy of the maths, and crossing.selftest.mjs holds it to 1,264 checks:
None of that proves the 2026 theorems. A finite search cannot. What it shows is that the drawings the theorems call optimal really achieve the claimed numbers, and that you cannot beat them by fiddling.