The crossing number of complete 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 graphs'. We prove the Harary–Hill conjecture: for every positive integer n, the ordinary crossing number of the complete graph Kn is \displaystyle \frac14\left\lfloor\frac n2\right\rfloor \left\lfloor\frac{n-1}{2}\right\rfloor \left\lfloor\frac{n-2}{2}\right\rfloor \left\lfloor\frac{n-3}{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