Harary–Hill and Zarankiewicz crossing-number conjectures (OpenAI, Lean)

Your AI and this story

Key facts

• Manuscripts: ‘The crossing number of complete graphs’ (abstract: ‘We prove the Harary–Hill conjecture: for every positive integer n, the ordinary crossing number of the complete graph Kn is ¼⌊n/2⌋⌊(n−1)/2⌋⌊(n−2)/2⌋⌊(n−3)/2⌋’) and ‘The crossing number of complete bipartite graphs’ (‘We prove the Zarankiewicz crossing-number conjecture, resolving Turán’s brickyard problem’), both ‘OpenAI, September 23, 2026’, family 165 of the 6 Oct release
• Convention: both papers count every crossing point (‘ordinary crossing number’), with no restriction on vertex positions or edge routes. Pair-crossing and odd-crossing variants are different quantities, and Balko extends the proof to some of them (pcr₊, ocr₊)
• Lean (OpenAI’s lean/docs/165.md): proves cr(K_n) = Z(n) for n ≥ 3, ‘the lower bound and … a matching two-page drawing’, and the Zarankiewicz equality for every positive m, n with an attaining drawing; crossings counted as spatial points of continuous simple edge paths. Comparator statements CompleteCrossing.lean and BipartiteCrossing.lean; both ‘accepted’ in the oai-math-revised comparator run of 25–26 Oct (which checks the proof against the challenge statement, not that the statement matches the paper)
• Balko’s exposition (arXiv 2610.34444, 25 Oct; Department of Applied Mathematics, Charles University): ‘In October 2026, OpenAI announced a proof of the Harary–Hill conjecture for all n, resolving the problem after more than 60 years. In this note, we present a simplified variant of this proof … The proof is based on the polynomial method … requires only elementary knowledge of linear algebra and graph theory.’ He also notes that ‘an independent exposition of OpenAI’s proof is being prepared by Gelasio Salazar’
• Balko’s AI statement (verbatim): ‘ChatGPT (OpenAI, Astra model) was used to assist in understanding the original proof, exploring possible simplifications of some of its arguments, improving the clarity and presentation of the text, and identifying relevant literature. All mathematical arguments were independently checked, rewritten, and verified by the author.’
• Human state of the art before the release (per Balko): proved for 2-page, shellable, x-monotone, bishellable, seq-shellable and spherical geodesic drawings; verified for n ≤ 14 by computer (2021); asymptotically cr(K_n) ≥ (0.985 + o(1))Z(n) (Balogh–Lidický–Salazar), improved to 0.9899. Zarankiewicz’s 1954 proof had a gap; the bipartite case was known for min(m, n) ≤ 6 (Kleitman) and some small cases
• Other reactions: Balogh, Layman, Lidický, Pfender, Salazar, Spiro and Volec (arXiv 2610.25204, 18 Oct) note that both conjectures ‘were claimed to be true in manuscripts by OpenAI dated Sep 23, 2026’ and describe their flag-algebra bounds as preceding them. Hubard, Ndiaye and Solé-Pi (2610.21017) note in a footnote that a solution was announced as their paper was about to appear. No refereed confirmation yet
• Digest: Dima Pasechnik’s ‘Crossing-number forest’ (28 Oct), a Stacks-project-style Forester site splitting the K_{m,n} paper into tagged definitions, lemmas and proof accounts mapped to the paper and to Lean declarations; it says its accounts reconstruct the paper’s proof and that Lean was not run locally (oai-math-revised NOTES, issue #56). Salazar’s Harary–Hill exposition not yet posted on 28 Oct