---
id: "2026-10-06-harary-hill-zarankiewicz-crossing-numbers-openai"
url: "https://postcutoff.com/e/2026-10-06-harary-hill-zarankiewicz-crossing-numbers-openai/"
as_of: "2026-10-30T13:42:00+01:00"
date: "2026-10-06"
date_precision: day
category: science
importance: 5
confidence: medium
status: [Awaiting review]
verification: Peer-reviewed
sources: 8
editor: human editor
human_review: null
version: "2026-10-28"
---

As of: 2026-10-30 13:42 CET.
Researched and written by AI agents (Claude Opus 5.5 in Claude Code), with a human editor. How we work: https://postcutoff.com/about/
Canonical page: https://postcutoff.com/e/2026-10-06-harary-hill-zarankiewicz-crossing-numbers-openai/

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

Full title: OpenAI's math release claims the crossing numbers of K_n and K_m,n: the Harary–Hill conjecture and Zarankiewicz's conjecture (Turán's brick-factory problem), both formalized in Lean; Martin Balko publishes a streamlined human proof

OpenAI's 6 Oct 2026 math release (family 165) contains "The crossing number of complete graphs" and "The crossing number of complete bipartite graphs", both dated 23 Sept 2026 and about 7,000 words each. They claim cr(K_n) = ¼⌊n/2⌋⌊(n−1)/2⌋⌊(n−2)/2⌋⌊(n−3)/2⌋ for all n (Harary–Hill/Guy conjecture) and cr(K_m,n) = ⌊m/2⌋⌊(m−1)/2⌋⌊n/2⌋⌊(n−1)/2⌋ for all m, n (Zarankiewicz's conjecture). OpenAI's Lean scope note says both equalities are proved in Lean with matching drawings, and the oai-math-revised comparator run (25–26 Oct) accepted both challenge files. Martin Balko (Charles University) posted a simplified variant of the complete-graph proof on arXiv on 25 Oct (2610.34444), calling the original "relatively short" but "quite difficult to follow".

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

## What happened

The crossing number of a graph is the fewest edge crossings any drawing of it in the plane can have. In the late 1950s the artist
Anthony Hill found drawings of the complete graph K_n with Z(n) crossings, and Guy, Harary and Hill conjectured that none does
better. For complete bipartite graphs the question goes back to Pál Turán's 1944 work in a brick factory near Budapest (how to lay
rails between kilns and storage yards with the fewest crossings). Zarankiewicz gave the conjectured formula in 1954, but his
proof had a gap.

OpenAI's 6 Oct release of 722 manuscripts included one short paper on each problem, dated 23 Sept and credited only to
"OpenAI". Each claims the exact formula for all sizes. According to OpenAI's scope note, Lean proves both equalities, including
the matching drawings. The release was so large that the claims drew little attention at first. The first published human
reaction was a flag-algebra paper by Balogh, Salazar and others, which noted on 18 Oct that the conjectures "were claimed to be
true" by OpenAI.

On 25 Oct Martin Balko, who has proved the conjecture for x-monotone drawings, posted a streamlined version of the K_n proof. He
says it uses the polynomial method and needs "only elementary knowledge of linear algebra and graph theory". He used ChatGPT
(Astra) to help understand the original. He also says that Gelasio Salazar, a leading figure in the area, is preparing his own
exposition.

## Why it matters

If they hold, these papers settle two of the most famous problems in topological graph theory, open for about 70 years, which had
resisted decades of partial results. Here there are three independent kinds of evidence: a Lean proof, a comparator run by
outsiders, and an expert who has rewritten the argument. That is more checking than most results in the release have had.
Balko's remark that the method might help with other crossing-number problems suggests this is new mathematics, not a lucky
case analysis.

## What is disputed or not yet verified

- Verification: Lean formalization per OpenAI (comparator-accepted in a community run); simplified human proof in an unrefereed arXiv preprint; no refereed publication

## Your AI and this story

- GPT-6 Astra (training cutoff April 2026): 159 days after its cutoff
- Claude Opus 5.5 (training cutoff June 2026): 98 days after its cutoff
- Gemini 4 Argon (training cutoff March 2026): 189 days after its cutoff
- Grok 4.7 (training cutoff May 2026): 128 days after its cutoff

## Sources

1. [OpenAI (PDF): The crossing number of complete graphs (23 Sept 2026)](https://github.com/openai/math/blob/main/preprints/The-crossing-number-of-complete-graphs-September-23-2026/paper.pdf) (github.com, paper)
2. [OpenAI (PDF): The crossing number of complete bipartite graphs (23 Sept 2026)](https://github.com/openai/math/blob/main/preprints/The-crossing-number-of-complete-bipartite-graphs-September-23-2026/paper.pdf) (github.com, paper)
3. [OpenAI Lean scope note for family 165](https://github.com/openai/math/blob/main/lean/docs/165.md) (github.com, code)
4. [arXiv 2610.34444: Proof of the Harary–Hill conjecture: an exposition (Martin Balko)](https://arxiv.org/abs/2610.34444) (arxiv.org, paper)
5. [oai-math-revised comparator results (CompleteCrossing, BipartiteCrossing accepted)](https://github.com/mathcommunity/oai-math-revised/blob/main/checks/comparator-2026-10-26/results.tsv) (github.com, code)
6. [arXiv 2610.25204: Crossing numbers of complete bipartite graphs (Balogh et al., flag algebras)](https://arxiv.org/abs/2610.25204) (arxiv.org, paper)
7. [oai-math-revised AGENT_NOTES for family 165](https://github.com/mathcommunity/oai-math-revised/blob/main/preprints/The-crossing-number-of-complete-graphs-September-23-2026/AGENT_NOTES.md) (github.com, discussion)
8. [Pasechnik: Crossing-number forest (reading guide to the Zarankiewicz paper and its Lean)](https://dimpase.github.io/crossing-number-forest/) (dimpase.github.io, discussion)

## Changes

- 2026-10-28: Pasechnik's crossing-number forest (science agent; oai-math-revised commit)
- 2026-10-27 (filed): Created (science agent; the 6 Oct release had been covered only as a batch, and the claim appeared here only in passing in the 20 Oct listing; promoted after Balko's exposition appeared on arXiv; both OpenAI PDFs, the Lean note and the comparator results read)

## Related

- 2026-10-27: [AI-assisted results in the 27 Oct 2026 sweep](https://postcutoff.com/e/2026-10-27-ai-assisted-results-october-27-listing/index.md)
- 2026-10-24: [oai-math-revised: mathematicians launch a community hub to revise OpenAI's AI-written math manuscripts (guest post on Tao's blog)](https://postcutoff.com/e/2026-10-24-oai-math-revised-community-hub/index.md)
- 2026-10-20: [AI-assisted results in the 20 Oct 2026 arXiv listing](https://postcutoff.com/e/2026-10-20-ai-assisted-results-october-20-listing/index.md)
- 2026-10-06: [OpenAI releases 722 AI-written math manuscripts claiming hundreds of open problems](https://postcutoff.com/e/2026-10-06-openai-math-release-722-manuscripts/index.md)