Subquadratic integrality gap for triangle packings

Open

Erdos81.triangle_packing_integrality_gap

by Yuning · Sep 8, 2026 · Mathlib 0df444a (Lean v4.33.1)

combinatoricsfractional-packingtriangle-packing

For every $\delta>0$ , all sufficiently large $n$ have the following uniform property. For every graph $G$ on $n$ vertices and every fractional triangle packing of total weight $W$ , there is an edge-disjoint integral triangle packing with at least

W-\delta n^2

triangles.

This is the fixed-family $F=K_3$ specialization of the asymptotic equality between fractional and integral graph-packing numbers.

Preamble

import Definitions.Def_Erdos81_triangle_packings

Formal statement

namespace Erdos81

/-- The fixed-triangle specialization of Yuster’s asymptotic equality between
fractional and integral graph packings. -/
theorem triangle_packing_integrality_gap :
    ∀ δ : ℝ, 0 < δ → ∃ n₀ : ℕ, ∀ n : ℕ, n₀ ≤ n →
      ∀ (G : SimpleGraph (Fin n)) (w : Finset (Fin n) → ℝ),
        IsFractionalTrianglePacking G w →
        ∃ T : Finset (Finset (Fin n)),
          IsTrianglePacking G T ∧
          fractionalTrianglePackingWeight w - δ * (n : ℝ) ^ 2 ≤ (T.card : ℝ) := by
  sorry

end Erdos81

Source

Raphael Yuster, Integer and fractional packing of families of graphs, arXiv:math/0305350v4, Theorem 1.2; https://arxiv.org/html/math/0305350v4#S1.Thmtheorem2

View graph