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 statement2 of 2

Upper bound (Davies–Illingworth 2022). There exists a constant $c_2 \ge 2$ such that, for sufficiently large $n$ , $f(n) \le c_2 \sqrt{\frac{n}{\log 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.upper1 lineExact file

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

SolvedStatement only, no proof