---

Claim. The statement of Problem 702 as the site prints it, with $k\ge4$ and no range on $n$, is false. For $n=5$ and $k=4$ the family of all five four-element subsets of a five-element set has $5>3=\binom32=\binom{n-2}{k-2}$ members, and any two of its members share three points, so no two meet in exactly one point. The Lean development Erdos702.lean in Boris Alexeev's repository of Lean proofs, added on 2026-08-18 and linked above at a pinned commit, records this as its named theorem not_erdos_702: the negation of the statement quantified over every $n$, every $k\ge4$ and every $k$-uniform family of subsets of Fin n with more than $\binom{n-2}{k-2}$ members, proved from the family allFourSubsetsOfFive by decidable checks of its size, its uniformity and its pairwise intersections; the alias erdos_702_all_n_false names the same theorem. The file's header names Frankl as the informal author and the AI systems Codex and GPT-5.6 Sol as its formal authors, and its module docstring presents the counterexample as the development's own record that the all-$n$ formulation is false; the submitter of the repository is the claimant here. The development's main theorem erdos_702_eventually is Frankl's eventual statement and is a formalization link on Frankl's claim page.

Depends on. No page of this wiki.

Why it is rejected. It answers the site's wording, not the corrected statement. Problem 702 judges the corrected Statement, which carries Erdős's own range $n>n_0(k)$ from his statements of the conjecture of Erdős and Sós; the problem page's Notes give the evidence. A failure at $n=5$ shows only that the threshold $n_0(4)$ is at least $5$, so the refutation settles no instance of the corrected Statement. The problem page's Notes credit the result.

Standing. The site's curator labels the problem proved and credits Frankl's theorem, so no outside reviewer has accepted a refutation of the problem. This corpus's verification built the Lean file at the pinned commit linked above and checked Erdos702.not_erdos_702: its axioms are exactly propext, Classical.choice and Quot.sound, and its statement matches the repository's comparator challenge ComparatorChallenges/ErdosProblems/Erdos702.lean. The theorem is correct, but it refutes only the site's wording, so the page stays rejected.