zarankiewicz_problem_k33
Disprovedcombinatoricsextremal-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
sorrySource