# The Harary–Hill and Zarankiewicz crossing-number formulas

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

- [The crossing number of complete graphs](../../preprints/The-crossing-number-of-complete-graphs-September-23-2026/paper.pdf)
- [The crossing number of complete bipartite graphs](../../preprints/The-crossing-number-of-complete-bipartite-graphs-September-23-2026/paper.pdf)

## 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

| Result | Comparator statement |
| --- | --- |
| Crossing number of complete graphs | [CompleteCrossing.lean](../ComparatorChallenges/CompleteCrossing.lean) |
| Crossing number of complete bipartite graphs | [BipartiteCrossing.lean](../ComparatorChallenges/BipartiteCrossing.lean) |