---

Claim. Write $I(k)$ for the number of irreducible covering sets of size $k$, $M(k)$ and $m(k)$ for the largest and smallest possible largest modulus, and $R(k)$ for the largest reciprocal sum, as in Problem 1189. The release asserts, with Lean 4 proofs, that $M(k)=3\cdot2^{k-3}$ for every $k\ge5$, sharpening Simpson's bound $n_k\le2^{k-1}$ to an exact value; that $k+1\le m(k)\le Ck(\log_2(k+1)+1)^6$ for an explicit constant $C$ and all large $k$, so $m(k)=k^{1+o(1)}$; that $R(k)=\Theta(\log k)$, with a harmonic-sum upper bound and an explicit base-$64$ construction; and that for every odd prime $p$ the divisors of $2^{p-1}p$ above one form an irreducible covering set, Sun's family, so the divisor question is answered yes. For the count it asserts

$$\log I(k)=\Bigl(\tfrac{4\sqrt\tau}{3}+o(1)\Bigr)k^{3/2}(\log k)^{-1/2}, \qquad \tau=\sum_{t\ge1}\log^2\bigl(1+\tfrac1t\bigr),$$

but what the Lean proves is the finite reduction count_answer_reduction: from a datum BBMSTLowerDatum n A B with $n\le k$, which packages a family of $A$ systems of size $n$ with distinct moduli, each counted at most $B$ times, from the frame construction of Balister, Bollobás, Morris, Sahasrabudhe and Tiba, and from BBMSTUpperHypothesis k U, an upper bound $U$ on the displayed minimal systems of size $k$, it concludes $A\le B\cdot I(k)$ and $I(k)\le U$. The asymptotic and its constant are not a Lean statement; they follow by hand from Theorem 1.1 of Balister, Bollobás, Morris, Sahasrabudhe and Tiba, a distinct-moduli bridging step that the release's own referee reports having checked by hand, and elementary estimates. The release says that nothing else in the four answers is conditional, and a later addition proves the lower half of the count, $\log I(k)\ge(\log2/4096)\,k\sqrt{k/\log(k+1)}$ along a sequence of sizes, without those hypotheses. The development distinguishes irreducibility from the irredundancy of one displayed cover, since a proper subset must fail to cover for every choice of residues, and it reports the exact values $I(5),\ldots,I(11)=1,4,15,65,318,2102,17040$, checked against an exhaustive census and an independent exact checker. The release names its principal theorems maximum_largest_modulus_answer, minimum_largest_modulus_answer, reciprocal_sum_answer and count_answer_reduction, reports a sorry-free build on Lean toolchain v4.31.0 with pinned Mathlib and the axioms propext, Classical.choice and Quot.sound, and describes an independent rebuild of the count's lower bound on separate hardware. Star Fleet Math, built by Colin Snyder, describes itself as a set of parallel agentic harnesses, each running a GPT-5.6 instance, with a separate proof-verifier harness running Claude Fable that reviews the answers, followed by a check by Snyder after its approval; the release credits the result to that system, and the Star Fleet Math listing states, without a reference, that van Doorn solved the problem first. The release carries no posting date of its own: its documentation is dated 13 July 2026, Pickhardt's manuscript dates the release to that day, and an update of the same day added the count's unconditional lower bound, so 2026-07-13 gives the page its date. The release is not on the site's proof-claims tab for the problem, where the one claim, by Pickhardt (claim page), notes in its own words that the comments and Star Fleet Math's proof were good and that its manuscript now supplies the full proof. Pickhardt's manuscript describes this development as concurrent work reaching the extremal answers but, in the form it cites, not the counting constant, and says that it found no verification in the published source that the frames survive the restriction to distinct moduli.

Depends on. Sun's theorem is the divisor family the development formalizes; the enumeration theorem of Balister, Bollobás, Morris, Sahasrabudhe and Tiba enters through the two stated hypotheses.

Standing. Claimed: the release is a web posting with a Lean bundle and no journal publication, referee report, curator acceptance or outside review located through 2026-10-06; the referee named in the release, the Claude Fable verifier harness followed by Snyder's own check, is part of the claimant's own system, not an independent reviewer. The site labels the problem OPEN (page last edited 8 April 2026). The Lean bundle is described, not built, replayed or audited by this corpus, so it is not counted as evidence.