---

Claim. Péter Frankl proves the conjecture of Erdős and Sós in On families of finite sets no two of which intersect in a singleton: for $k\ge4$ and $n>n_0(k)$, every family $\mathcal F$ of $k$-element subsets of an $n$-element set with $|\mathcal F|>\binom{n-2}{k-2}$ contains two members $A,B$ with $|A\cap B|=1$. The threshold is sharp, since the $\binom{n-2}{k-2}$ sets containing a fixed pair pairwise meet in at least two points. Theorem 2 of the paper (printed p. 132) gives the explicit range $n>n_0(k)+2\binom{n_0(k)}{k}$ and the structure at the threshold: a family with no two members meeting in one point has fewer than $\binom{n-2}{k-2}$ members or is exactly the family of all $k$-sets through a fixed pair. The proof analyzes the links $\mathcal F_x$ and their $\Delta$-systems (sunflowers). Katona had proved the case $k=4$; his proof is unpublished and the site records it without a source. For $k=3$ the analogous statement fails, as Erdős and Sós observed, since there are $n$ triples on $n$ points with no two meeting in one point when $4\mid n$.

Formulation. This is the corrected Statement of Problem 702, which carries Erdős's own range $n>n_0(k)$, and the claim is full for it. The site's wording drops that range and is false for $k+1\le n\le3k-4$, as the problem page's Notes record; Frankl's theorem says nothing about those $n$.

Acceptance. Refereed, reviewed and formalized. Refereed: Bull. Austral. Math. Soc. 17 (1977), no. 1, 125–134; the issue is dated August 1977, and the page is dated to the first day of that month. Reviewed: Thomas Bloom, the site's curator, marks the problem proved and credits the proof for all $k\ge4$ to Frankl [Fr77]. The library card records the paper's results; no proof review is recorded.

Formalized: this corpus's verification built Boris Alexeev's repository of Lean proofs at its pinned commit of 2026-09-15, linked above, in its src/latest folder (Lean v4.33.0, Mathlib v4.33.0), whose module ErdosProblems.Erdos702, with its import ErdosProblems.Erdos703.Iteration, is the development added on 2026-08-18, changed since only by a header, the repository's comparator guidelines and linting, and checked the axioms of Erdos702.erdos_702_eventually, which are exactly propext, Classical.choice and Quot.sound. The repository's comparator challenge ComparatorChallenges/ErdosProblems/Erdos702.lean pins that theorem together with the definitions its type reaches (IsUniform, that every member has $k$ elements; HasSingletonIntersection, that two members meet in exactly one point; and twoStarBound, $\binom{n-2}{k-2}$), and the fingerprint of the built theorem was found identical to the challenge. The statement was audited clause by clause against the corrected Statement: subsets of Fin n stand for subsets of $\{1,\ldots,n\}$; both require $k\ge4$; a threshold $n_0$ with the conclusion for every $n\ge n_0$ is equivalent to one with the conclusion for $n>n_0(k)$; the bound is $\binom{n-2}{k-2}$, and the truncated subtraction $n-2$ matters only for $n\le1$, where no family meets the hypothesis; and the conclusion allows $A=B$, which cannot meet itself in one point since $|A|=k\ge4$. The theorem is therefore the corrected Statement, and the module's source closure contains no sorry, no axiom and no native_decide. The build certifies that statement only: it does not formalize the structure clause of Theorem 2, that at the threshold the family of all $k$-sets through a fixed pair is the only extremal family, which rests on the refereed paper alone.

Formalization. Boris Alexeev's repository holds a Lean 4 development, added on 2026-08-18, whose header calls it a formalization of a solution to the problem, names Frankl as the informal author and the AI systems Codex and GPT-5.6 Sol as the formal authors, and cites a write-up tex/702.tex for the mathematical proof and the formalization map. Its main theorem is the eventual statement: for every $k\ge4$ there is $n_0$ such that for $n\ge n_0$ a family of $k$-element subsets of an $n$-element set with more than $\binom{n-2}{k-2}$ members has two members meeting in exactly one point. A second named theorem records that the site's wording, with no range on $n$, fails, with the family of all four-element subsets of a five-element set as the counterexample; it is not Frankl's result and is recorded on a rejected claim page. This corpus's verification built and audited that development, its main theorem is the corrected Statement, and the page carries formalized evidence for it, as the Acceptance section records.