Open. The site labels the problem OPEN (page last edited 8 April 2026). Its commentary records the last question as settled by Sun, whose theorem that the divisors of $2^{p-1}p$ above one form an irreducible covering set for every odd prime $p$ is the accepted partial claim on Sun's claim page (2006); it also records Simpson's bound $n_k\le2^{k-1}$, the accepted partial claim on Simpson's claim page (1985), and the upper bound of Balister, Bollobás, Morris, Sahasrabudhe and Tiba on the number of irreducible covering sets of size $k$, the accepted partial claim on their claim page (Balister, Bollobás, Morris, Sahasrabudhe and Tiba, 2019). Two full claims are recorded without adoption. The proof-claims tab carries one, on Pickhardt's claim page (2026): the count of irreducible covering sets of size $k$ with the sharp constant $4\sqrt\tau/3$ in its exponent, the largest modulus exactly $3\cdot2^{k-3}$, the smallest $k^{1+o(1)}$ and the maximum reciprocal sum of order $\log k$ (manuscript of 2026-07-22 co-authored with the Omniscience Research Agent, submitted 2026-07-28 by Jeff Pickhardt). The other, on Snyder's claim page (2026), is a Lean 4 development released on Star Fleet Math on 2026-07-13 by Colin Snyder and produced by that system's GPT-5.6 harness: the same extremal answers and Sun's family, and, for the count, a Lean reduction to two hypotheses, a distinct-moduli frame datum and an upper count of displayed minimal systems, from which the asymptotic with its constant follows by hand from Theorem 1.1 of Balister, Bollobás, Morris, Sahasrabudhe and Tiba, a distinct-moduli bridging step the release's referee checked by hand, and elementary estimates; it is not on the proof-claims tab, whose one claim refers to it. The standing is claimed through those pending full claims; no outside review is recorded for either.