Solved. Alon and Erdős ([AlEr96], refereed) proved $f(n)=n^{1/3+o(1)}$, with $n^{1/3}/(\log n)^{4/3}\ll f(n)\ll n^{1/3}(\log\log n)^{1/3}/(\log n)^{1/3}$; Vu ([Vu07], refereed) raised the lower bound to $f(n)\gg n^{1/3}/\log n$; and Conlon, Fox and Pham ([CFP21], Theorem 1.5, to appear in J. Eur. Math. Soc.) determined the order of growth, $f(n)\asymp n^{1/3}(n/\phi(n))/((\log n)^{1/3}(\log\log n)^{2/3})$. The site's commentary records the first two bounds as proved and credits the order of growth to Conlon, Fox and Pham, on a page labeled SOLVED. The first two are accepted partial claims (Alon and Erdős, Vu), and the third is the accepted full claim (claim page (Conlon, Fox and Pham, 2021)), whose acceptance evidence is the site's documented acceptance, the journal version having no record yet. A 2026 Lean formalization of the Conlon–Fox–Pham order in Boris Alexeev's public repository, registered by no outside record, attributes its mathematics to the three authors, so it is a formalization link on their claim page, neither built nor audited here, and gives no formalized evidence.