---

Claim. The site's wording is false. For every $d\ge0$ there is a $3$-uniform hypergraph on $23\cdot23^d$ vertices with $92\cdot(23^d)^2$ edges in which no three edges span at most five vertices, so

$$\mathrm{ex}_3(n,\mathcal F_5)\ge\frac{92}{529}\,n^2>\frac{n^2}6 \qquad\text{for } n=23^{d+1},$$

and $\mathrm{ex}_3(n,\mathcal F_k)/n^2\to1/6$ fails at $k=5$; the file's theorem not_erdos_1076 negates the assertion for every $k\ge5$ of the site's wording of Problem 1076, with $\mathcal F_k$-freeness defined as no $k-2$ edges spanning at most $k$ vertices, the single family that wording defines. The construction replaces every block of an explicit packing of an eleven-edge support graph by four triples; the packing comes from a cyclic graceful labeling over $\mathbb Z/23$ and a two-column orthogonal array. The bound $92/529$ is weaker than the true limit $1/5$ of Glock 2019, which the file's docstring cites as the known value, but the file states that its disproof is self-contained and does not rely on Glock's approximate packing theorem, so it is an independent proof and not a formalization of Glock's result.

Claimant. The file in Boris Alexeev's lean-proofs collection was added on 17 August 2026 under the authors Boris Alexeev and Codex; the header added on 23 August 2026 names Stefan Glock as the informal author and Codex and GPT-5.6 Sol as the formal authors. The collection's record page for the problem, linked above, presents the file as a formalized proof of the problem.

Why it is rejected. It answers the site's wording, the single family $\mathcal F_k$, not the corrected Statement of Problem 1076, whose family is cumulative: not_erdos_1076 negates the single-family assertion, and under the corrected Statement a $3$-graph avoiding $\mathcal F_4\cup\mathcal F_5$ is linear, so the construction says nothing against it, and the page does not count toward the problem's standing. The development is third-party Lean the corpus has not built, so whether its proof is correct is not checked here; it is not refereed, and the site does not cite it. The refereed results of Glock 2019 and Glock, Joos, Kim, Kühn, Lichev and Pikhurko 2024 refute the site's wording independently of this file.