AI Proved What?

Episode 165, October 2026

Brickyard solved?

Two preprints claim the exact crossing numbers of all complete and complete bipartite graphs, proving the Harary–Hill and Zarankiewicz conjectures

Covers result 165 in OpenAI’s catalog: all 2 papers. See its connections to other results and the work it cites.

Play Episode 165: Brickyard solved? Five orange kilns and five teal yards on two axes joined by blue tracks, with the 16 crossings marked in red (our drawing).

5:53. English captions available. The video loads from YouTube when you press play.

Chapters

  1. 0:00The problem
  2. 1:49The claim
  3. 3:07How the proof goes
  4. 5:12Where it stands

The claim, in plain words

Draw a graph in the plane with its edges as curves. The crossing number cr(G) is the fewest crossings any drawing can have; in the papers’ words, edges are “simple continuous arcs”, crossings are proper, and c(D) counts crossing points, “counting every crossing when two edges meet repeatedly”, with “no restriction on vertex positions or edge routes”. For the complete bipartite graph Km,n, the question is Turán’s brickyard problem, which began, as the paper recounts, with rail connections between kilns and storage yards at a brick factory near Budapest in 1944. Zarankiewicz’s axis drawing has ⌊m/2⌋⌊(m−1)/2⌋⌊n/2⌋⌊(n−1)/2⌋ crossings, “but the published argument for its optimality contained a gap”. For the complete graph Kn, Hill’s number ¼⌊n/2⌋⌊(n−1)/2⌋⌊(n−2)/2⌋⌊(n−3)/2⌋ is attained by classic drawings, and Harary and Hill conjectured it is optimal (Guy’s 1960 note gave the first published upper bound). As the papers recount, Kleitman proved the bipartite formula when one side has at most six vertices; Pan and Richter’s computer-assisted proof gave cr(K11) = 100, Aichholzer reported cr(K13) = 225, and Woodall verified K7,7 and K7,9 by computation; the strongest general bounds they cite are a ratio above 0.98559895 for Kn and cr(Kn,n) ≥ 0.9118 times the conjectured value, asymptotically.

Result 165 rests on two OpenAI preprints, both dated September 23, 2026. The crossing number of complete graphs (13 pages), Theorem 1.1: “For every integer n ≥ 3, cr(Kn) = ¼⌊n/2⌋⌊(n−1)/2⌋⌊(n−2)/2⌋⌊(n−3)/2⌋”, which “resolves the Harary–Hill conjecture positively”. The crossing number of complete bipartite graphs (16 pages), Theorem 1.1: “For all positive integers m, n, cr(Km,n) = dmdn”, with dr = ⌊r/2⌋⌊(r−1)/2⌋, resolving “the Zarankiewicz crossing-number conjecture positively”. So, for example, cr(K7) = 9, cr(K11) = 100, cr(K5,5) = 16 and cr(K9,9) = 256.

What it doesn’t claim

The papers concern the ordinary crossing number only, not the pair, odd or straight-line versions, and drawings in the plane, not other surfaces. They do not classify the optimal drawings. The upper bounds are well-known drawings: Zarankiewicz’s axis drawing, and a two-page drawing that de Klerk, Pasechnik and Salazar presented, building on book drawings of Blažek and Koman and of Damiani, D’Antona and Salemi. Neither theorem is derived from the other (“The lower bound does not depend on the bipartite crossing-number formula”), though the complete-graph paper adapts the companion’s tools and re-proves what it uses; no computer search is involved. Both papers mention earlier published claims of both formulas by Hebbar and Mangam; the complete-graph paper notes that “counting crossings in prescribed drawings gives upper bounds; establishing the minimum over all drawings also requires a lower-bound argument.”

Where it stands

Posted as preprints
OpenAI, 13 and 16 pages, both dated September 23, 2026
Peer reviewed
Not yet
Checked in Lean
Both theorems exactly, under the standard definition. We have not rebuilt it

Last checked October 19, 2026. Neither preprint has been revised since it was added to the repository in its initial commit on October 6, 2026. OpenAI published a Lean formalization with one comparator per paper (complete graphs, complete bipartite graphs): vertices at distinct points, edges as injective continuous paths avoiding other vertices, finitely many proper crossings defined by local charts, no triple points, and crossing points counted. By our count the proofs take 385 files and 38,663 lines excluding Mathlib (complete-graph development, bipartite development and shared geometry). We found no unproved steps, and we have not rebuilt it. Neither paper is among those OSVerify reviewed, and we have seen no expert review.

How the proof goes

  1. Normalize and keep signed books. A minimum drawing can be made polygonal with no crossings between edges that share an endpoint. Direct the edges, give each crossing a sign by orientation, and record the counterclockwise order of edges at each vertex.
  2. Loops cross zero times net. Two closed polygonal walks have total signed intersection zero; with half-weighted corrections where two cycles share a vertex, this gives J(z, z′) = 0 for every pair of cycles (the “cycle pairing”).
  3. Complete graphs, odd n = 2s + 1. Label the vertices by distinct reals. Polynomials in the four endpoints of a pair of edges, symmetric within each edge and of degree at most s − 2 in each variable, form a space of dimension exactly (s choose 2)², Hill’s number. Evaluating them on the edge pairs with nonzero signed count is injective with a totally isotropic image, so those pairs, and hence the crossings, number at least Hill’s number.
  4. Complete bipartite graphs, odd n = 2s + 1. A detector turns the signed counts between the fans of two kilns into an s² × s² matrix whose rank is at most their number of crossings, with full rank for a fan against itself. An inequality about subspaces, proved in the paper, forces the ranks to sum to at least twice Zarankiewicz’s number.
  5. Even sizes. Delete each vertex in turn and average; the odd formulas give the even ones exactly.

The numbers in the video

  • Our exact counts: Zarankiewicz’s axis drawing of K5,5 has 16 crossings; the two-page drawing of K7 has 2 above the spine and 7 below, 9 in all; the two-page counts equal Hill’s number for n = 3 to 30.
  • Our check of the cycle identity, in exact arithmetic, on all pairs of triangles in random drawings of K6 and K7 with straight edges (12 and 23 crossing points) and of K6 with two bends per edge (186 crossing points, with pairs crossing up to six times): no exception.
  • The K7 basis {1, x+u, xu} ⊗ {1, y+v, yv}, nine polynomials; in the 5 × 5 axis drawing, fans of kilns on the same side cross 4 times and on opposite sides 0 times (ours), the equality case of the rank bound by our reckoning.
  • The Lean counts: 385 files and about 39,000 lines, our count of the two import closures.

Read the source

The 2 papers in this result

OpenAI groups related papers, such as alternative proofs, supporting results and consequences, into one result; we label the first paper it lists the main paper and the others companions.

Transcript

Read the full script

0:00The problem

Put n dots in the plane and join every pair by a curve. The curves may wiggle anywhere, but each crossing costs one, and the crossing number is the fewest crossings any drawing can get away with. Five dots already force one crossing. The bipartite version is older. It comes from Turán: as the paper recounts, it began with rail tracks between kilns and storage yards at a brick factory near Budapest in 1944: join every kiln to every yard, with as few track crossings as possible. There are classic drawings. Put the kilns on a vertical line and the yards on a horizontal line, each split as evenly as possible across the centre, and use straight tracks. Five kilns and five yards then cross sixteen times, and in general the count is Zarankiewicz’s number. He published a proof that this is best, but it contained a gap. For n dots, Hill’s formula, a quarter of the product of the halves of n, n minus one, n minus two and n minus three, each rounded down, is attained, for example, by putting the dots on a line and drawing each edge as an arch, above or below by a simple rule on the dots’ labels: seven dots, nine crossings. Harary and Hill conjectured that nothing does better. A good drawing only gives an upper bound; a lower bound must beat every possible drawing. As the papers recount, Kleitman proved the bipartite formula when one side has at most six vertices, computer-assisted proofs settled eleven dots and seven kilns with seven or nine yards, and one was reported for thirteen dots. In general, the strongest bounds the papers cite reached about ninety-eight and a half percent of Hill’s number, and about ninety-one percent of Zarankiewicz’s for equal sides, in the limit.

1:49The claim

Result 165 rests on two OpenAI preprints, both dated September 23: 13 pages on complete graphs, and 16 on complete bipartite graphs. The first proves that for every n of at least three, the crossing number of n dots, all joined, is exactly Hill’s number. The second proves that for all m and n, m kilns and n yards need exactly Zarankiewicz’s number of crossings. Both use the standard definition: edges are any continuous curves that never cross themselves, and every crossing point counts, even when two edges cross repeatedly. If the proofs hold, the classic drawings are optimal and both conjectures are true. The papers do not classify the best drawings, and they treat only drawings in the plane, not other surfaces. Their drawings are well-known ones: Zarankiewicz’s own, and a two-page drawing that de Klerk, Pasechnik and Salazar presented, building on earlier book drawings. Neither theorem is derived from the other, though they share tools, and no computer search is involved. Both papers also mention earlier published claims of both formulas; the first notes that counting the crossings of particular drawings only gives upper bounds.

3:07How the proof goes

Both proofs first simplify a best drawing, so that edges sharing an endpoint never cross. Then give each edge a direction, score each crossing plus or minus one according to which way the second edge passes, and at every vertex record the counterclockwise order of its edges. The key fact is that two closed loops in the plane cross zero times net. Applied to cycles of edges, with half-credit corrections where two cycles meet at a vertex, it gives one exact equation for every pair of cycles. In our check, these equations held exactly on random drawings, including messy ones where two edges cross up to six times. For an odd number of dots, two s plus one, label the dots with distinct numbers and look at polynomials in the four endpoints of a pair of edges, symmetric within each edge, with degree at most s minus two in each variable. A basis of them has exactly Hill’s number of members: for seven dots, three times three, nine. Evaluate them on the pairs of edges with a nonzero signed count. The cycle equations, used with polynomial weights, show that this evaluation loses nothing, and that its image fills at most half of the available room. So there are at least as many crossings as basis polynomials. Even sizes follow by deleting each vertex in turn and averaging. For kilns and yards, with an odd number of yards, the crossings are grouped by which two kilns’ fans of track they involve. A detector turns each group’s signed counts into a square matrix whose rank is at most the number of crossings in it, while a fan compared with itself gives full rank. An inequality about subspaces, proved in the paper, then forces the ranks to add up to at least twice Zarankiewicz’s number, and even numbers of yards again follow by deletion. In the five-by-five axis drawing, fans on the same side cross four times each and fans on opposite sides not at all; by our reckoning, that is exactly the extreme case of the inequality.

5:12Where it stands

Both papers are preprints, not peer reviewed and not revised since release. OpenAI’s Lean formalization states both theorems exactly, with edges as continuous paths that never cross themselves and every crossing point counted, and proves them in about 39,000 lines, by our count. We found no unproved steps, and we have not rebuilt it. Neither paper is among those OSVerify reviewed, and we have seen no expert review. If the proofs hold, two problems from the 1940s, 1950s and 1960s are settled: the brick-factory tracks, and the dots on a page, can do no better than the classic drawings.

Spot a mistake?

This episode simplifies on purpose, but it shouldn’t be wrong. If something is, open an issue on GitHub or leave a comment on YouTube. Corrections are noted here with a date.