∑math20

Combinatorics · Result 165

The Harary–Hill and Zarankiewicz crossing-number formulas

2 papersLean

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.

Watch

▶Introduction: the problem and why it mattersin preparation
▶The presented solutionin preparation

Papers 2

First page of The crossing number of complete graphs

The crossing number of complete graphs

OpenAI · September 23, 2026

We prove the Harary–Hill conjecture: for every positive integer n, the ordinary crossing number of the complete graph Kn is \(\displaystyle \frac14\left\lfloor\frac n2\right\rfloor \left\lfloor\frac{n-1}{2}\right\rfloor \left\lfloor\frac{n-2}{2}\right\rfloor \left\lfloor\frac{n-3}{2}\right\rfloor.\)

Read PDF Download Source

Cite
@misc{OAI:The-crossing-number-of-complete-graphs-September-23-2026,
  author = {{OpenAI}},
  title = {{The crossing number of complete graphs}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-crossing-number-of-complete-graphs-September-23-2026/paper.pdf}{OAI:The-crossing-number-of-complete-graphs-September-23-2026}},
  year = {2026}
}
First page of The crossing number of complete bipartite graphs

The crossing number of complete bipartite graphs

OpenAI · September 23, 2026

We prove the Zarankiewicz crossing-number conjecture, resolving Turán's brickyard problem. For all positive integers m, n, the ordinary crossing number of the complete bipartite graph \(K_{m,n}\) is \(\displaystyle \left\lfloor\frac m2\right\rfloor \left\lfloor\frac{m-1}{2}\right\rfloor \left\lfloor\frac n2\right\rfloor \left\lfloor\frac{n-1}{2}\right\rfloor.\)

Read PDF Download Source

Cite
@misc{OAI:The-crossing-number-of-complete-bipartite-graphs-September-23-2026,
  author = {{OpenAI}},
  title = {{The crossing number of complete bipartite graphs}},
  howpublished = {OpenAI Math Release preprint
                  \href{https://github.com/openai/math/blob/main/preprints/The-crossing-number-of-complete-bipartite-graphs-September-23-2026/paper.pdf}{OAI:The-crossing-number-of-complete-bipartite-graphs-September-23-2026}},
  year = {2026}
}

What was formalized in Lean

The following describes the scope of the Lean formalization related to the following accompanying paper(s):

Scope

The formalized result proves Hill's proposed formula for the crossing number of the complete graph: for every \(n\ge3\), \(\mathrm{cr}(K_n)=\frac14\lfloor n/2\rfloor\lfloor(n-1)/2\rfloor\lfloor(n-2)/2\rfloor\lfloor(n-3)/2\rfloor\). It proves the lower bound and constructs a matching two-page drawing. Crossings are spatial points, so repeated crossings of one edge pair count separately.

Zarankiewicz's crossing-number conjecture predicts \(\mathrm{cr}(K_{m,n})=\lfloor m/2\rfloor\lfloor(m-1)/2\rfloor\lfloor n/2\rfloor\lfloor(n-1)/2\rfloor\). The formalized result proves this equality for every positive \(m,n\) and constructs a drawing attaining it. Crossings are counted as spatial points for continuous simple edge paths, including repeated crossings between the same pair of edges.

Comparator links

ResultComparator statement
Crossing number of complete graphsCompleteCrossing.lean
Crossing number of complete bipartite graphsBipartiteCrossing.lean

Scope note on GitHub →