Erdos Problem 81: n²/6 plus a linear remainder
OpenErdos81.root_problemThere are universal constants and such that every finite chordal graph on vertices has an exact edge partition into at most
complete subgraphs. The constants are chosen independently of and , and the pieces partition edges rather than merely cover them.
import Definitions.Def_erdos81_clique_partitions
namespace Erdos81
/-- Erdős Problem 81: a universal linear remainder above `n²/6`. -/
theorem root_problem :
∃ C : ℝ, 0 < C ∧ ∃ n₀ : ℕ, 1 ≤ n₀ ∧
∀ n : ℕ, n₀ ≤ n → ∀ G : SimpleGraph (Fin n),
IsChordal G →
HasCliquePartitionAtMost G ((n : ℝ) ^ 2 / 6 + C * n) := by sorry
end Erdos81Read-back
What the Lean code literally says, in plain math · gpt-5.6-luna
There exists a real number C with C greater than 0 and there exists a natural number n₀ with 1 ≤ n₀ such that, for every natural number n with n₀ ≤ n and every simple graph G whose vertex set is Fin n, if there exists an injective natural-number rank assignment in which any two distinct neighbors of each vertex having larger rank than that vertex are adjacent, then there exists a finite collection P of finite vertex sets such that every member of P is a clique, every edge of G belongs to exactly one member of P, and the real-valued number of members of P is at most the square of n regarded as a real number divided by 6, plus C multiplied by n regarded as a real number.
Confirmed by the mission captain (proposal self-audit).