Overview. Crossing numbers of complete bipartite graphs: a reading forest [index]
Overview. Crossing numbers of complete bipartite graphs: a reading forest [index]
Deployed from my github repo. Please feel free to leave your comments there.
A structured reading of the paper [cn-0042] and its proof of the Zarankiewicz formula:
\[\operatorname {cr}(K_{m,n})=\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 .\]Start here. The proof introduction [cn-0070] explains the route from subspaces to crossings, introducing notation before use. The guided reading [cn-0001] includes it with the main statement and final proof assembly. The main theorem [cn-0007] links its complete argument, and the Lean guide [cn-0038] maps the paper's lemmas to formal declarations.
- Algebra: subspace interpolation and the rank-sum inequality [cn-0061].
- Topology: normalize a drawing and derive the additive block relation [cn-0060].
- The detector: barycentric weights and two-triangle interpolation [cn-0062].
- Odd-size lower bound [cn-0035], even-size deletion [cn-0037], and the matching upper bound [cn-0036].
- An exact four-by-four example [cn-0040], sources and checks [cn-0039], and references [cn-0041].
Definition index. Each concept below has a permanent tag and is linked at its points of use.
- Complete bipartite graphs and stars [cn-0002].
- Continuous plane drawings [cn-0003].
- Proper crossings and admissible drawings [cn-0004].
- Crossing count and ordinary crossing number [cn-0005].
- Independent crossing count and crossing number [cn-0066].
- Balanced pair counts and the Zarankiewicz number [cn-0006].
- Normalized drawings [cn-0008].
- Signed interior intersections [cn-0010].
- Polygonal walks and their mutual signed intersection [cn-0069].
- Spoke orders and half-order matrices [cn-0011].
- Endpoint coefficients of an oriented chord [cn-0068].
- Signed edge vectors of cycles [cn-0012].
- The endpoint-corrected intersection matrix [cn-0013].
- Row-plus-column matrices [cn-0017].
- Interpolation nodes [cn-0063].
- Univariate polynomial maps into a vector space [cn-0064].
- Polynomial constraints and evaluation filtrations [cn-0019].
- Graphs of linear maps [cn-0026].
- Bivariate evaluation vectors and the two triangles [cn-0028].
- Barycentric interpolation weights [cn-0030].
- The rank detector and its atoms [cn-0032].
Status. The mathematical results are labelled proof-account: they reconstruct the pinned paper's proof. Exact finite examples and static Lean source checks are recorded separately. No local Lean or Comparator run is claimed. Details of the verification scope [cn-0039].
License. The forest's original notes and code are licensed under Apache 2.0. The source attribution and notices describe the material adapted from OpenAI and the included third-party components.
- Proof dependencies
- None.
- Provenance
- Reading project based on the OpenAI preprint of 23 September 2026 and its accompanying Lean sources, pinned on 9 October 2026.