OpenAI. The crossing number of complete bipartite graphs. Preprint, 23 September 2026, 16 pages. Repository directory; local PDF; LaTeX entry point; original bibliography.

Theorem 1.1 is the formula [cn-0007]. The proof's main components are Lemma 2.1 [cn-0024], Corollary 2.3 [cn-0027], Lemmas 3.1–3.2 [cn-0060], Lemmas 4.1–4.2 [cn-0062], and normalization in Appendix A [cn-0009]. The source record [cn-0039] identifies the archived version and local checks.

For a comparison with Scott and Wilmer [cn-0071], see the exterior-algebra note [cn-0072]. It gives a short coordinate-case proof [cn-0073] and an ambient-dimension refinement [cn-0074], and explains which obstacles remain to using those methods in place of the general subspace argument.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

OpenAI math repository, Crossing Lean development, commit fd4aeeb2ee4fc729c18d98444fed42fd0529eeeb. Local Main.lean; formalization catalogue; Comparator configuration.

The reading guide [cn-0038] maps paper results to declarations. The verification record [cn-0039] reports the static checks performed here and distinguishes them from local compilation and formal verification. The archived toolchain is Lean 4.34.1 with Mathlib commit d13f23b723b8a846827a245b89c10fc7d3f11612, as recorded in lakefile.lean and lake-manifest.json.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 1. József Balogh, Bernard Lidický, Sergey Norin, Florian Pfender, Gelasio Salazar, and Sam Spiro. Crossing numbers of complete bipartite graphs. Procedia Computer Science 223 (2023), 78–87. Source.

Historical lower bound cited in the introduction.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 2. Jean-Paul Berrut and Lloyd N. Trefethen. Barycentric Lagrange interpolation. SIAM Review 46(3) (2004), 501–517. Source.

Sections 2–3, especially equation (3.2), provide the classical weights [cn-0030].

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 3. Daniel Brosch and Sven C. Polak. New lower bounds on crossing numbers of K(m,n) from semidefinite programming. Mathematical Programming 207 (2024), 693–715. Source.

Historical refinement of fixed-part-size lower bounds cited in the introduction.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 4. E. de Klerk, J. Maharry, D. V. Pasechnik, R. B. Richter, and G. Salazar. Improved bounds for the crossing numbers of K(m,n) and K(n). SIAM Journal on Discrete Mathematics 20(1) (2006), 189–202. Source.

Cited as reference 4 in the introduction for semidefinite lower bounds using rotation constraints.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 5. Etienne de Klerk, Dmitrii V. Pasechnik, and Alexander Schrijver. Reduction of symmetric semidefinite programs using the regular *-representation. Mathematical Programming 109(2–3) (2007), 613–624. Source.

Cited as reference 5 in the introduction for symmetry reduction in semidefinite crossing-number bounds.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 6. Paul Erdős and Richard K. Guy. Crossing number problems. The American Mathematical Monthly 80(1) (1973), 52–58. Source.

Historical context for the gap in the original optimality argument.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 7. Radoslav Fulek, Michael J. Pelsmajer, Marcus Schaefer, and Daniel Štefankovič. Adjacent crossings do matter. Journal of Graph Algorithms and Applications 16(3) (2012), 759–782. Source. Archived PDF.

Section 1, p. 760, distinguishes prohibiting adjacent crossings from allowing them without counting them. The first restriction preserves the ordinary crossing number [cn-0005], as in normalization [cn-0009]. The second gives the independent crossing number [cn-0066], and the authors explicitly leave equality with the ordinary crossing number open, even for complete graphs. Their separations concern odd and algebraic crossing-number variants; they do not provide a counterexample to \(\operatorname {cr}=\operatorname {cr}_-\).

For a later statement of the complete-graph question, see Schaefer's July 2026 survey [cn-0067], Question 2, p. 103. The scope of the September 2026 bipartite argument is explained at its lower-bound step [cn-0035].

Proof dependencies

None.

Provenance

Bibliographic entry from the pinned paper; abstract and Section 1, pp. 759–760, consulted on 9 October 2026.

Paper reference 8. Venkatesan Guruswami and Swastik Kopparty. Explicit subspace designs. Combinatorica 36(2) (2016), 161–185. Source.

Background comparison for determinant multiplicity in the subspace inequality [cn-0024], whose proof is supplied separately.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 9. Sanjith Hebbar and Tabitha Agnes Mangam. Crossing numbers of complete bipartite graphs and complete graphs. International Journal of Engineering and Technology 7(4) (2018), 2996–3000. Source.

Mentioned as earlier published claims; no result from this paper is used in the proof account.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 10. Daniel J. Kleitman. The crossing number of K(5,n). Journal of Combinatorial Theory 9(4) (1970), 315–323. Source.

Section 8, equation (17), is cited for local cyclic-order arguments; Section 3, equations (6)–(7), for vertex deletion [cn-0037].

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 11. János Pach and Géza Tóth. Which crossing number is it anyway?. Journal of Combinatorial Theory, Series B 80(2) (2000), 225–246. Source.

Background for the distinction between point counts [cn-0005], pair counts, and parity counts.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 12. Alexander A. Razborov. Flag algebras. The Journal of Symbolic Logic 72(4) (2007), 1239–1282. Source.

Methodological background for earlier balanced-graph lower bounds cited in the introduction.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 13. Paul Turán. A note of welcome. Journal of Graph Theory 1(1) (1977), 7–9. Source.

Pages 8–9 are cited for the brickyard origin of the problem.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 14. W. T. Tutte. Toward a theory of crossing numbers. Journal of Combinatorial Theory 8(1) (1970), 45–53. Source.

Historical background for algebraic approaches to crossing numbers.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 15. D. R. Woodall. Cyclic-order graphs and Zarankiewicz’s crossing-number conjecture. Journal of Graph Theory 17(6) (1993), 657–671. Source.

Page 658 is cited for the axis construction [cn-0036]; Theorem 1 and Corollary 1.1 for vertex deletion [cn-0037].

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Paper reference 16. Casimir Zarankiewicz. On a problem of P. Turan concerning graphs. Fundamenta Mathematicae 41(1) (1955), 137–145. Source.

Source of the classical balanced-axis upper bound [cn-0036]; the introduction distinguishes that construction from the incomplete original optimality argument.

Proof dependencies

None.

Provenance

Expository organization and source review, 9 October 2026.

Marcus Schaefer. The Graph Crossing Number and its Variants: A Survey. The Electronic Journal of Combinatorics, Dynamic Survey 21, ninth edition, 17 July 2026. Publisher. Archived edition.

The entry on p. 62 defines the independent crossing number [cn-0066]. Question 2 on p. 103 asks whether \(\operatorname {cr}(K_n)=\operatorname {cr}_-(K_n)\); the discussion continues on p. 104. This edition therefore records the complete-graph question as open in July 2026.

That date precedes the September 2026 OpenAI papers. For the specific limitation of the bipartite proof studied here, see the scope of normalization [cn-0009] and the diagonal-block step in the lower bound [cn-0035].

Proof dependencies

None.

Provenance

Ninth edition, 17 July 2026; pp. 62 and 103–104 consulted on 9 October 2026.

Alex Scott and Elizabeth Wilmer. Combinatorics in the exterior algebra and the Bollobás Two Families Theorem. Journal of the London Mathematical Society 104(4) (2021), 1812–1839. Publisher and DOI. Version read; full text.

The relevant parts are Section 2.1 on initial monomials, Lemma 3.1 on generic projections, and Theorem 4.5 on weighted subspace pairs. Numbered locators here refer to the linked preprint version. The comparison [cn-0072] explains their relation to the subspace-intersection inequality [cn-0024]. Lemma 3.1 also yields an ambient-dimension refinement [cn-0074].

Proof dependencies

None.

Provenance

Bibliographic details checked against the publisher; mathematical comparison based on arXiv:1907.06019v2, 14 July 2020, read on 12 October 2026.