---

Claim. Call a family of subsets of $\{1,\ldots,n\}$ admissible for $r$ when no member contains another and every size that occurs among its members occurs at least $r$ times, and let $n_0(r)$ be the least $N$ such that for every $n>N$ some admissible family has exactly $n-3$ distinct sizes. The manuscript states that

$$n_0(r)=2r+4\quad(4\le r\le 10),\qquad n_0(r)=2r+5\quad(r\ge 11).$$

Together with the values $n_0(2)=3$ and $n_0(3)=8$ computed by He and Tang ([HeTa26b] on the problem page; the source card records them), this gives $n_0(r)$ for every $r\ge2$, which answers Problem 776 under either reading; the values sit inside He and Tang's bounds $2r+2\le n_0(r)\le 2r+2\log_2 r+O(\log\log r)$. As the forum entry describes the argument, the Kruskal–Katona theorem gives exact shadow constraints between consecutive size levels; for $r\ge11$, estimates on the low levels and an obstruction spanning four levels confine a carry $e$ to $1\le e\le6$: the lower bound $e\ge1$ excludes an admissible family with $n-3$ sizes at $n=2r+5$, and the upper bound $e\le6$ leaves a feasible core, which is punctured and then padded two points at a time to build families for every larger $n$; for $4\le r\le10$ the same constraints and constructions are verified by exact finite computation. The forum entry adds that the Lean development proves the set-family theorem for every $r\ge4$, with three bounded ranges closed by finite evaluation through soundness bridges proved in Lean.

Submission note. Posted to erdosproblems.com as a proof claim by AI's operated by M.Thiim (account mthiim) on 17 July 2026, giving "All ideas and lean formalization due to LLM's - exact contribution of each is specified in submission package. LLM's used: OpenAI ChatGPT 5.6 Pro, Anthropic Claude Fable 5, OpenAI Codex w gpt-5.6-Sol-Max" as the AI used:

Erdős #776 asks when subsets of $[n]$ can occupy $n-3$ sizes, with no set contained in another and at least $r$ sets at each occupied size. Let $n_0(r)$ be the least $N$ working for every $n>N$. We prove $n_0(r)=2r+4$ for $4\le r\le10$ and $n_0(r)=2r+5$ for $r\ge11$. Combining with $n_0(2)=3$ and $n_0(3)=8$, due to Yixin He and Quanyu Tang (as discussed in forum), this completes the table for $r\ge2$ with exact proven values. Kruskal--Katona gives exact shadow constraints between successive size levels. For $r\ge11$, lower-level estimates and a four-level obstruction give a carry $1\le e\le6$. Here $e\ge1$ rules out $n=2r+5$, while $e\le6$ yields a feasible core; puncturing and repeated two-point padding then construct examples for every larger $n$. The cases $4\le r\le10$ use exact finite checks of the same constraints and constructions. Lean proves the full set-family theorem for $r\ge4$; only three bounded ranges use finite evaluation, through proved soundness bridges. Notes: Whole proof package can be found on Github. This includes a README.md that serves as a useful entropy pint for the problem statement, links to paper, notes that can be useful to validating the proof and the lean formalization: https://github.com/mthiim/erdos_776/. Tag: v0.4.1-proof-claim, commit hash: 1ca43203123642edaac45bf00b6fc333c848b4c9

Depends on. [[problems/set_systems/E0776/claims/2026_02_10_he_tang|He and Tang's thresholds at r equal to 2 and 3]]: the values $n_0(2)=3$ and $n_0(3)=8$, which the manuscript cites and its Lean development does not formalize, so the table for every $r\ge2$ is complete only with that pending claim.

Claimant. M. Thiim, posting under the username mthiim on 17 July 2026, who presents the result as the work of language models they operated (OpenAI ChatGPT 5.6 Pro, Anthropic Claude Fable 5, and OpenAI Codex with gpt-5.6-Sol-Max), with the contribution of each recorded in the repository's credits file; the page is named for the human submitter, who published the claim. The manuscript is the PDF in the repository at the claim's tag.

Formalization. The repository at the claim's tag (the pinned commit above) declares a Lean proof of the set-family theorem for every $r\ge4$, with $n_0(r)$ stated as genuine leastness. Its README reports that the ranges $4\le r\le10$, $11\le r\le28$ and $29\le r\le377$ are closed by native_decide evaluations tied to the combinatorial statements by soundness bridges proved in Lean, that the range $r\ge378$ is proved symbolically, and that no source uses sorry or a project axiom; the complete endpoints additionally carry the three native_decide certificate axioms, trusting Lean's compiler, while only the symbolic $r\ge378$ endpoint rests on the standard axioms alone. The values for $r=2,3$ are not part of that development and rest on He and Tang's computation.

Acceptance. None that counts as evidence. The manuscript is not refereed, and the site labels the problem OPEN (page last edited 10 April 2026) and does not credit this result. The forum thread carries three comments: on 21 July 2026 a forum user reported an independent check, building the Lean project from a cold cache with no errors and no sorry, reproducing the axiom audit, reading the statement file against the site's wording, re-implementing the Kruskal–Katona cascade to reproduce the boundary numbers and checking the stored $r=11$ certificate, and said the check convinced them; the claimant replied the same day; a comment of 19 August 2026 asked whether anyone had read the human-readable PDF. A pseudonymous forum check is not a named outside reviewer, so no reviewed evidence is listed, and no Lean audited by the corpus checks the result, so no formalized evidence is listed. A further replication, posted in the problem's thread on 6 September 2026, rederives the cases $r=5$, $6$ and $11$ with Lean lemmas that import this development; it is recorded on the problem page and is not outside evidence either. The partial claim Ronen's value n_0(4)=12 agrees with this result at $r=4$.