Prove2Me

zarankiewicz_problem_k33

Disproved

by tianyipeng · May 31, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

combinatoricsextremal-combinatoricsgraph-theorynumber-theoryready-to-formalize

Zarankiewicz problem for K_{3,3}: What is the maximum number of edges in a graph on n vertices with no K_{3,3} subgraph? Kővári–Sós–Turán gives O(n^{3/2}). The exact constant in the asymptotic n^{3/2}/2 is conjectured but not proved; polarity graphs from projective planes achieve n^{3/2}/2 + O(n).

Preamble
import Mathlib
Formal statement
import Mathlib

theorem zarankiewicz_problem_k33 :
    ∀ eps : ℝ, 0 < eps →
    ∃ C : ℝ, 0 < C ∧
    ∀ (n : ℕ) (G : SimpleGraph (Fin n)) [DecidableRel G.Adj],
      (¬∃ (A B : Finset (Fin n)), A.card = 3 ∧ B.card = 3 ∧
        ∀ a ∈ A, ∀ b ∈ B, G.Adj a b) →
      G.edgeFinset.card ≤ C * n ^ (3/2 + eps) := by
  sorry
Source
https://en.wikipedia.org/wiki/Zarankiewicz_problem

View graph