Dense regime of Erdős Problem 81

Open

Erdos81.dense_chordal_clique_partition

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

chordal-graphsclique-partitioncombinatoricsgraph-theoryopen-problem

There are universal constants $C>0$ and $n_0\ge1$ such that the following holds. Let $G$ be a chordal graph on $n\ge n_0$ vertices. If the canonical partition that treats every edge as its own two-vertex clique contains more than

\frac{n^2}{6}+Cn

parts, then the edges of $G$ nevertheless admit an exact partition into at most that many cliques by grouping suitable edges into larger complete subgraphs.

This is the dense, genuinely compressive regime of Erdős Problem 81. The complementary regime needs no chordality: the canonical one-clique-per-edge partition already meets the requested bound. This theorem remains an open subproblem rather than a claimed consequence of the existing literature.

Preamble

import Definitions.Def_erdos81_clique_partitions
import Definitions.Def_Erdos81_edgePairPartition

Formal statement

namespace Erdos81

/-- The hard regime of Erdős Problem 81: when the canonical one-clique-per-edge
partition is too large, larger cliques compress it to the conjectured bound. -/
theorem dense_chordal_clique_partition :
    ∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, 1 ≤ n₀ ∧
      ∀ n : ℕ, n₀ ≤ n → ∀ G : SimpleGraph (Fin n),
        IsChordal G →
        ((edgePairPartition G).card : ℝ) > (n : ℝ) ^ 2 / 6 + C * n →
        HasCliquePartitionAtMost G ((n : ℝ) ^ 2 / 6 + C * n) := by
  sorry

end Erdos81

Source

Open dense-case restriction of Erdős Problem 81, https://www.erdosproblems.com/81; motivated by Erdős–Ordman–Zalcstein, Clique Partitions of Chordal Graphs, Combinatorics, Probability and Computing 2 (1993), 409–415, https://doi.org/10.1017/S0963548300000808. This restriction is proposed as an open reduction child and is not attributed as a proved theorem to that paper.

View graph