The crossing number of complete bipartite graphs

Lean formalization in OpenAI math repository (Result 165)

Model / AI: OpenAI (unreleased)

OpenAI's internal frontier model proved and formalized in Lean the main result of 'The crossing number of complete bipartite graphs'. We prove the Zarankiewicz crossing-number conjecture, resolving Turán's brickyard problem. For all positive integers m, n, the ordinary crossing number of the complete bipartite graph K_{m,n} is \displaystyle \left\lfloor\frac m2\right\rfloor \left\lfloor\frac{m-1}{2}\right\rfloor \left\lfloor\frac n2\right\rfloor \left\lfloor\frac{n-1}{2}\right\rfloor.

Source read 2026-10-08. Cataloged from OpenAI's formalization.yaml (Family 165). The Lean development was not rebuilt locally.

• Paper — Paper
• Lean — Lean formalization note
• Code — OpenAI math repository