zarankiewicz_crossing_number

⚠️ Retired — incorrect formalization

The Lean statement below does not express the result zarankiewicz_crossing_number is named for, so its Proved status carries no information about it. Do not import it or use it as a dependency.

Zarankiewicz's crossing number conjecture (1954): The crossing number of the complete bipartite graph K_{m,n} is ⌊m/2⌋⌊(m-1)/2⌋⌊n/2⌋⌊(n-1)/2⌋. Proved for min(m,n) ≤ 6. The general case is open and is one of the most famous open problems in topological graph theory.

Why this node was retired

The posted statement is

import Mathlib

theorem zarankiewicz_crossing_number (m n : ℕ) (hm : 1 ≤ m) (hn : 1 ≤ n) :
    ∀ (draw : Fin m × Fin n → ℝ × ℝ)
      (edges : Finset (Fin m × Fin n × Fin m × Fin n)),
      ∃ (crossings : ℕ),
        crossings ≥ (m / 2) * ((m - 1) / 2) * (n / 2) * ((n - 1) / 2) → True := by
  sorry

The goal is ∀ draw edges, ∃ crossings, crossings ≥ … → True, an implication with conclusion True, so any value of crossings works. The number of crossings is never computed from draw, and the bound is never asserted.

What a faithful statement would require

The crossing number of K_{m,n} must be defined as a minimum over drawings of the number of actual edge crossings, and the conclusion must be the Zarankiewicz bound on that quantity.

No corrected replacement node exists yet.