---

Claim. The answer to Problem 775 is no. Theorem 1.1 of Gao's paper states that for every $k\ge3$ and every constant $C\ge0$ there is $N(k,C)$ such that every $k$-uniform hypergraph on $n\ge N(k,C)$ vertices has at most $n-C$ distinct sizes of cliques, a clique being a maximal complete subhypergraph. Writing $g(n,k)$ for the largest number of distinct clique sizes in a $k$-uniform hypergraph on $n$ vertices, this says $g(n,k)\le n-\omega(1)$, so for $k=3$ no constant $C$ admits a $3$-uniform hypergraph on $n$ vertices with $n-C$ distinct clique sizes for infinitely many $n$. The site's commentary records that Erdős had constructed $3$-uniform hypergraphs with at least $n-\log_* n$ distinct clique sizes, so the gap between $n$ and $g(n,3)$ grows, but slowly. The graph case is different: there $g(n,2)=n-\log_2 n+O(1)$, the lower bound by Spencer and the upper bound by Moon and Moser, both on refereed pages linked from the problem page.

The proof introduces $(k,C)$-layered trees, trees with a vertex ordering $v_0,\dots,v_t$ in which every vertex is adjacent to an earlier one, every vertex lies within distance $k$ of $v_0$, and the degree of $v_i$ is at most $2^{C+i}$. Lemma 2.2 shows by induction on $k$ that such a tree has a bounded number of vertices, and a hypergraph with too many distinct clique sizes is shown to contain a layered tree larger than that bound. The source card holds the digest.

Claimant. Jun Gao, On cliques in hypergraphs, arXiv:2510.14804, posted 16 October 2025 (v1), revised 17 October (v2) and 31 October 2025 (v3). The arXiv record lists no journal reference, so the paper is not recorded as refereed.

Acceptance. The site's curator, Thomas Bloom, lists Problem 775 as disproved and credits the negative answer to Gao [Ga25], in the general form the commentary states, that the number of distinct clique sizes in a $k$-uniform hypergraph on $n$ vertices falls short of $n$ by an unbounded amount (reviewed). The paper was reported in the problem's forum thread on 17 October 2025, and the site's page was updated to credit it.

Formalization. The Lean file among the links, in Boris Alexeev's repository lean-proofs, declares itself a formalization of a solution to Problem 775, naming Jun Gao as its informal author and Aristotle and Lorenzo Luccioli as its formal authors; it formalizes Theorem 1.1 as main_theorem and the $k=3$ specialization as erdos_problem_775. Luccioli announced the formalization in the problem's forum thread on 19 April 2026, with the code at the gist among the links, pinned to the revision they posted, and the repository copy is pinned to the commit of 24 June 2026 that last touched its path. A later forum comment of 3 June 2026 reports that the gist did not compile under Lean v4.28.1 and offers a patched copy; that copy is not a posting of the claimant's result and is not linked. This corpus has not built any of these files, so the formalization is a link and not formalized evidence. The formal-conjectures statement file for the problem marks it solved and points at the repository copy; a statement file is not a formalization.