The Harary–Hill and Zarankiewicz crossing-number conjectures
The Harary–Hill conjecture asserts that the crossing number of the complete graph Kn is Z(n) = ¼⌊n/2⌋⌊(n−1)/2⌋⌊(n−2)/2⌋⌊(n−3)/2⌋, and Zarankiewicz's crossing-number conjecture, the formulation of Turán's brick factory problem, asserts that the crossing number of the complete bipartite graph Km,n is ⌊m/2⌋⌊(m−1)/2⌋⌊n/2⌋⌊(n−1)/2⌋. Two manuscripts dated 23 September 2026 in OpenAI's public mathematics collection (github.com/openai/math) claim proofs of both formulas for unrestricted drawings, with a Lean formalization of both. This page summarizes the published claims and lists publicly available follow-up work. Statements are the respective authors' claims; the publication of a paper, code or a formal proof is not presented here as independent verification.
Background
- As recounted in the introductions of the two manuscripts:
- The ordinary crossing number is the minimum, over all plane drawings with simple continuous arcs, of the number of crossing points, so that two edges crossing several times count several times. Other crossing parameters count each crossing pair of edges once, or only pairs crossing an odd number of times, and differ from this one; the manuscripts cite Pach and Tóth and Fulek and coauthors for the distinction.
- Turán described the origin of the bipartite problem in rail connections at a brick factory near Budapest in 1944. Zarankiewicz supplied the balanced construction, but his published argument for its optimality contained a gap. Kleitman proved the formula when one vertex class has at most six vertices, and Woodall verified K7,7 and K7,9 by computation with cyclic-order graphs. Semidefinite lower bounds were obtained by de Klerk and coauthors and refined by Brosch and Polak, and Balogh, Lidický, Norin, Pfender, Salazar and Spiro proved cr(Kn,n) ≥ 0.9118 times the conjectured value asymptotically, using flag algebras.
- Harary and Hill described Hill's construction for Kn and stated the conjectured formula in 1963, crediting Guy's 1960 note with the first published upper bound. Pan and Richter's computer-assisted proof gave cr(K11) = 100 and hence cr(K12) = 150, and Aichholzer reported a computer-assisted proof of cr(K13) = 225. Asymptotically, de Klerk, Maharry, Pasechnik, Richter and Salazar obtained a ratio of at least 0.83 to the conjectured value, and Balogh, Lidický and Salazar a ratio greater than 0.98559895.
- The lower bound was known for restricted drawing classes: two-page drawings, by Ábrego, Aichholzer, Fernández-Merchant, Ramos and Salazar, then shellable drawings, which include cylindrical and x-bounded drawings, and spherical geodesic drawings of points in general position, by Streltsova and Wagner. Both manuscripts also note that Hebbar and Mangam published claims of both formulas, and the complete-graph manuscript remarks that counting the crossings of prescribed drawings gives upper bounds only.
The original result
- Claim. Theorem 1.1 of the complete-graph manuscript states that cr(Kn) = Z(n) for every n ≥ 3, which resolves the Harary–Hill conjecture. Theorem 1.1 of the bipartite manuscript states that cr(Km,n) = dmdn with dr = ⌊r/2⌋⌊(r−1)/2⌋ for all positive integers m and n, which resolves Zarankiewicz's conjecture. Both statements concern unrestricted drawings with curved edges and repeated crossings.
- Method, as described: both lower bounds combine signed intersection counts of edges with a correction from the cyclic order of edges at a common endpoint, which gives a pairing that vanishes on pairs of cycles. In the bipartite case a subspace inequality, ∑ dim(Ui ∩ Vj) ≤ ⌊m2/4⌋N whenever Ui ∩ Vi = 0, proved by polynomial interpolation, and a linear order detector turn this pairing into a rank-sum bound. In the complete case, polynomials in four variables of degree at most s − 2 in each variable, a space of dimension Z(2s + 1), are evaluated at ordered pairs of independent edges with a nonzero signed crossing count. An even-node detector shows that this evaluation is injective, and the image is totally isotropic for a nondegenerate symmetric form, so its dimension is at most half the number of coordinates, and each supported pair of edges requires a crossing. Even orders follow by vertex deletion, and classical drawings give the matching upper bounds. The complete-graph manuscript states that its lower bound does not depend on the bipartite formula.
- Sources. The manuscripts The crossing number of complete graphs and The crossing number of complete bipartite graphs.
- Formalization, as described by the repository. The scope note lean/docs/165.md states that the formalization proves Hill's formula for every n ≥ 3, with the lower bound and a matching two-page drawing, and Zarankiewicz's formula for all positive m and n, with a drawing attaining it. In both, crossings are counted as points for continuous simple edge paths, including repeated crossings of the same pair of edges. The Comparator statements are CompleteCrossing.lean and BipartiteCrossing.lean.
Public follow-up work
| Date | Work | Relation | Public claim | Public status (checked 18 October 2026) |
|---|---|---|---|---|
| 2026-10-06 | THM-922, update of 6 October 2026, in the GitHub repository eliottcassidy2000/math | Use (conditional) | Taking the bipartite formula as correct, the record concludes that the two-page Zarankiewicz conjecture of de Klerk, Pasechnik and Salazar holds for all m and n. It also gives an explicit form, by parity classes on a cyclic spine, of a two-page drawing of Km,m with exactly Z(m,m) crossings, and notes that this upper bound itself is classical. | A record in a multi-agent AI research repository. It labels its lower bound as conditional on the OpenAI family and states that the Lean formalization was not rebuilt there. |
| 2026-10-08 | MathVet (GitHub, review of openai/math, tables at repository commit c76f1e4, 14 October 2026) |
Review (fidelity of the formal statements) | Rates the family "full": the two Lean theorems state both formulas for all sizes, for drawings by arbitrary continuous simple arcs with crossings counted as points. The minimum ranges over a custom class of admissible drawings, with finitely many crossing points, each topologically transversal, and no triple points, which MathVet calls the usual crossing-number class. It records sandboxed Comparator passes for both challenges. | MathVet states that its ratings concern whether the Lean states the headline claims. |
| 2026-10-10 | cert-machine, openai/math lane K, runs 38017370880 and 38051470892 | Verification (two kernels) | Records that Lean's default kernel and the nanoda kernel accept the BipartiteCrossing solution in 309 seconds and the CompleteCrossing solution in 430 seconds. |
Repository. |
| 2026-10-10 to 2026-10-14 | con-leche development journal (task #348) | Verification (second kernel) | In its run over all Comparator challenges of the collection at commit fd4aeeb, the journal's table of exceptions lists neither CompleteCrossing nor BipartiteCrossing, so both challenges were accepted by con-leche and by Lean's official kernel. |
Development journal. |
| 2026-10-12 | dimpase/crossing-number-forest (GitHub; Dima Pasechnik and contributors, as stated in its notice), published at dimpase.github.io/crossing-number-forest | Reading (exposition) | A linked Forester reading guide to the bipartite manuscript and its Lean development at commit fd4aeeb, with written-out proof accounts, exact-arithmetic checks of small cases and a source-level check of the Lean files. Editorial notes compare the subspace inequality with the exterior-algebra methods of Scott and Wilmer, give a short proof when all subspaces are spanned by subsets of one basis, and refine the bound by replacing the ambient dimension with the largest dim Ui + dim Vi. |
The guide states that its finite checks illustrate the arguments and do not prove the formula, and that its Lean source check does not run Lean or Comparator. |
| 2026-10-14 | A. Hubard, C. S. Ndiaye and O. Solé-Pi, arXiv 2610.21017v1, Crossing numbers of simplicial complexes | Related work | Studies crossing numbers of d-dimensional simplicial complexes in dimension 2d, including a generalized Harary–Hill conjecture, and gives a simple proof of the Harary–Hill conjecture for antipodal drawings. A footnote states that a solution to the Zarankiewicz and Hill conjectures was announced when the manuscript was about to be made public, and that the text was not otherwise revised; it does not name the announcement. | arXiv preprint, version 1. |
Notes
- The list covers follow-ups found in public sources up to the date above; it is not a priority or completeness claim.