---

Claim. $g(n)\gg n^{1/2}$: for every $f$ from the pairs of $\{1,\ldots,n\}$ to $\{1,\ldots,n\}$ with $f(x,y)\notin\{x,y\}$ there is an independent set of size at least $c\,n^{1/2}$, for an absolute $c>0$. Spencer [Sp72] proves an extension of Turán's theorem to $r$-uniform hypergraphs by the probabilistic method: a hypergraph with $n$ vertices and $t$ edges has an independent set of order at least $c_r\,n^{1+1/(r-1)}/t^{1/(r-1)}$. Applied to the $3$-uniform hypergraph on $\{1,\ldots,n\}$ whose edges are the triples $\{x,y,f(x,y)\}$, at most $\binom n2$ of them, this gives an independent set of order $n^{3/2}/n=n^{1/2}$, and a set that contains no such triple is independent for $f$. Spencer's paper treats the general set-mapping function of Erdős and Hajnal [ErHa58], of which $g(n)$ is the case of pairs mapped to single points; it improves Erdős and Hajnal's own lower bound $n^{1/3}$. The paper is not held in the library; its theorem is stated as the site, Conlon, Fox and Sudakov, and Füredi state it, Füredi's form being that a $3$-uniform hypergraph on $n$ vertices with average degree $d$ has an independent set of size at least $c\,n/\sqrt d$ (inequality (2.4), in the proof of Theorem 2.3 of Maximal independent subsets in Steiner systems and in planar sets).

Covers. The lower bound $g(n)\gg n^{1/2}$. The matching upper bound is the claim of Conlon, Fox and Sudakov and, earlier, of Füredi 1991.

Acceptance. Refereed: Joel Spencer, Turán's theorem for $k$-graphs, Discrete Math. 2 (1972), no. 2, 183–186; the record gives the issue month, May 1972, and no day, so the page is dated to the first day of that month. Reviewed: Thomas Bloom, the site's curator, labels the problem solved and credits Spencer with the lower bound $g(n)\gg n^{1/2}$. Nothing here rests on this project's own review.

Formalization. The Lean development Erdos1025 released by IIIS Lean, among the links at its commit of 15 September 2026 and cited by the community database as the problem's Lean formalization, says in its README that it formalizes the known square-root lower and upper bounds, that its Erdos1025.lower_bound follows Spencer's three-uniform independent-set method with Rödl, Sales and Zhao's account as a modern reference, and that it was produced with AI assistance through Lean Constellation (Codex and, where used, Grok), IIIS Lean being responsible for the packaging and verification and claiming no independent expert audit. The corpus has not built it, so it is a link and not formalized evidence; Alexeev's Lean file, whose lower bound is also Spencer's argument, is linked from the page of Conlon, Fox and Sudakov.