---

Claim. The answer to Problem 722 is yes: for fixed $k>r\ge1$ there is $n_0(k,r)$ such that for every $n>n_0$ satisfying $\binom{k-i}{r-i}\mid\binom{n-i}{r-i}$ for all $0\le i<r$ there is a family of $k$-subsets of $\{1,\ldots,n\}$ containing every $r$-subset exactly once, an $r$-$(n,k,1)$ design or Steiner system $S(r,k,n)$. This is the existence conjecture for designs, in Keevash's The existence of designs (card). It is the case $G=K_n^r$ of Keevash's Theorem 1.4, which gives a $K_q^r$-decomposition of every $K_q^r$-divisible, typical $r$-uniform hypergraph $G$ on $n>n_0$ vertices with density at least $n^{-\alpha}$; Theorem 1.10 extends the conclusion to designs of any fixed multiplicity $\lambda$. The method, randomized algebraic construction, builds an approximate decomposition and absorbs the leftover with algebraically structured configurations. Before it, the question was settled only for small parameters: Kirkman for $(r,k)=(2,3)$, Hanani for $(3,4)$, $(2,4)$ and $(2,5)$, and Wilson for $(2,k)$ with every $k$, each with its own claim page. An independent second proof, by iterative absorption, is Glock, Kühn, Lo and Osthus's designs by iterative absorption.

Acceptance. Reviewed: the site's curator, Thomas Bloom, labels the problem proved and credits the general case to Keevash [Ke14], independently of its author; Glock, Kühn, Lo and Osthus's refereed memoir presents its own argument as a new proof of Keevash's theorem. The preprint is arXiv:1401.3665, posted 2014-01-15, the date of this page; its fourth version (2024-11-27) says it incorporates referee comments, but the arXiv record lists no journal reference, so the page lists no refereed evidence. The proof was not reconstructed in this corpus.

Formalization. Boris Alexeev's repository holds a Lean 4 development, added on 2026-08-20, whose header calls it a formalization of a solution to the problem, names Peter Keevash as the informal author and "Codex" and "GPT-5.6 Sol" as the formal authors. Its top-level theorem erdos_722 states the problem in the problem's own form: for all $0<r<k$ there is $n_0$ such that every $n\ge n_0$ satisfying $\binom{k-i}{r-i}\mid\binom{n-i}{r-i}$ for all $i<r$ carries a family of $k$-subsets of an $n$-element set containing each $r$-subset exactly once; the argument is carried in separate modules, and the file is linked above at its commit. This corpus has not built or audited that development, so the page lists no formalized evidence; the acceptance rests on the curator's credit.