crossing_number_complete_graph

⚠️ Retired — incorrect formalization

The Lean statement below does not express the problem its name refers to, so its Disproved status carries no information about that problem. Do not import it or use it as a dependency.

Zarankiewicz / Guy conjecture for complete graphs: the crossing number of $K_n$ is conjectured to be

Why this node was retired

The defect is in the preamble, not in the theorem line. crossingNumber is defined as

noncomputable def crossingNumber (n : ℕ) : ℕ :=
    sInf {c : ℕ | ∃ (draw : Fin n × Fin n → ℝ × ℝ) (cross : Finset (Sym2 (Sym2 (Fin n)))),
      cross.card = c ∧ True}

Nothing in this set constrains cross to be the set of crossings of draw — the only condition on it is cross.card = c ∧ True, and draw is an arbitrary map with no planarity or edge-geometry attached. Taking draw constant and cross = ∅ puts $0$ in the set for every $n$, so crossingNumber n = 0 identically.

The theorem therefore asserts that the Zarankiewicz expression is $0$ for all $n$, which fails already at $n = 5$ (the expression is $1$). Its Disproved status is a fact about this placeholder definition; the Zarankiewicz–Guy conjecture itself is open (it is known for $n \le 12$).

What a faithful statement would require

crossingNumber must be defined as the minimum, over drawings of $K_n$ in the plane, of the number of actual pairwise edge crossings — which requires modelling edges as curves and crossings as transversal intersection points.

No corrected replacement node exists yet.