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.