Erdős problem 1104

Lower bound (Hefty–Horn–King–Pfender 2025). There exists a constant $c_1 \in (0,1]$ such that, for sufficiently large $n$ , $c_1 \sqrt{\frac{n}{\log n}} \le f(n),$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as `triangleFreeMaxChromatic n`.

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

1104.lean

Retained formal statement1 of 2

Lower bound (Hefty–Horn–King–Pfender 2025). There exists a constant $c_1 \in (0,1]$ such that, for sufficiently large $n$ , $c_1 \sqrt{\frac{n}{\log n}} \le f(n),$ where $f(n)$ denotes the maximum chromatic number of a triangle-free graph on $n$ vertices, formalized as triangleFreeMaxChromatic n.

FormalConjectures/ErdosProblems/1104.leanErdos1104.erdos_1104.variants.lower1 lineExact file

1∃ c₁, 0 < c₁ ∧ c₁ ≤ 1 ∧ ∀ᶠ (n : ℕ) in Filter.atTop, c₁ * √↑n / √(Real.log ↑n) ≤ ↑(Erdos1104.triangleFreeMaxChromatic n)

SolvedStatement only, no proof