The site's wording quantifies over every $n$ and fails for small $n$. At $k=4$, $n=5$ the five $4$-element subsets of $\{1,\ldots,5\}$ pairwise share three points, and $5>3=\binom32$; this failure is the theorem not_erdos_702 described below. Such failures lie at the smallest values of $n$, which is the range the poser's texts exclude.

The change inserts "and $n>n_0(k)$", Erdős's own range, in which $n_0(k)$ is a threshold depending only on $k$, so the corrected Statement asserts that some such threshold exists; nothing else changes. The evidence is Erdős's own statements of the conjecture of Erdős and Sós. [Er75f], §6, printed p. 108 (On some problems of elementary and combinatorial geometry): "We conjectured that if $l>3$, $A_i\subset S$, $1\leqslant i\leqslant k$, $|A_i|=l$, $n>n_0(l)$, $k>\binom{n-2}{l-2}$ then for some $1\leqslant i<j\leqslant k$, $|A_i\cap A_j|=1$." [Er76b], item 22, printed p. 186 (Problems and results in graph theory and combinatorial analysis), where $f(n;k,r)$ is the least size of a family of $k$-subsets of an $n$-set that forces two members with exactly $r$ common elements: "V.T. Sós and I conjectured four years ago that if $k > 3$, $n > n_0(k)$ then (1) $f(n;k,1) = \binom{n-2}{k-2} + 1$." [Er82e], Chapter III, §6, printed p. 72 (Some of my favourite problems which recently have been solved), states the conjecture "for $n > n_0(k)$" as $\mathrm{Max}\,t_k=\binom{n-2}{k-2}$ and reports "(1) was proved for $k = 4$ by Katona and by P. Frankl in the general case." [Er81], Part I, item 5 (On the combinatorial problems which I would most like to see solved), states the conjecture with no range on $n$ and reports it proved "by P. Frankl [45] for all $k$"; the omission is already in that text, and the site's wording, which agrees with the other three in everything but the range, omits it too. The site's own credit to Frankl [Fr77] for all $k\ge4$ and Frankl's statement of the conjecture with $n>n_0(k)$ (p. 125, citing [Er76b]) agree with these texts. The form comes from these texts, not from the range of any theorem that settles it.

The all-$n$ failure is the named theorem not_erdos_702 of the Lean development Erdos702.lean in Boris Alexeev's repository of Lean proofs, added on 2026-08-18 (pinned file), whose header names the AI systems Codex and GPT-5.6 Sol as its formal authors; it proves the failure at $n=5$, $k=4$. The theorem is correct, but it answers the site's wording (every $n$), not the corrected Statement ($n>n_0(k)$), so it does not count toward the problem's standing; it is credited here and on its rejected claim page (Alexeev, 2026).