Erdős–Rogers problem: largest triangle-free induced subgraph forced in a $K_4$-free graph (Erdős #620)

Let $f(n)$ be the largest integer such that every $K_4$-free graph on $n$ vertices (no four mutually adjacent vertices) contains an induced subgraph on at least $f(n)$ vertices that is triangle-free (contains no $K_3$). Equivalently: how large a triangle-free induced subgraph is guaranteed inside any $n$-vertex graph with no $K_4$? Determine the growth rate of $f(n)$. It is known that $f(n)=n^{1/2+o(1)}$; the open problem is to pin down the lower-order (polylogarithmic) factors, and in particular to close the gap between the best current lower and upper bounds.

Acceptance. FULLY RESOLVES: determine the asymptotics of $f(n)$ up to constant factors — a proof establishing $f(n)=\Theta\big(n^{1/2}g(n)\big)$ for an explicit polylogarithmic $g$, i.e. matching lower and upper bounds agreeing up to constants (machine-checkable proof preferred, else a complete written proof). ADVANCES: prove a new bound on $f(n)$ that strictly improves the current record stated in the background — a lower bound better than $n^{1/2}(\log n)^{1/2}/\log\log n$, or an upper bound better than $n^{1/2}\log n$ — with a full proof; a construction-based upper bound must be accompanied by an explicit (possibly randomized) $K_4$-free graph family together with a proof that its largest triangle-free induced subgraph is as small as claimed. Deliver the proof (and, for constructions, the graph family and the bound it certifies).