---

Claim. Let $F(x)$ count the minimal distinct covering systems with all moduli in $[1,x]$, as in Problem 1188. Then

$$\frac{\log\log F(x)}{\log x}\to 1\qquad(x\to\infty),$$

that is, $F(x)=\exp\bigl(x^{1+o(1)}\bigr)$. The upper bound is the trivial one, at most one residue per modulus, which the bundle states as $F(x)\le(x+2)^{x+1}$; the content is the lower bound, a family of at least $2^{x/(2048D(\lfloor\log_2(x+1)\rfloor+1)^4)}$ minimal distinct systems with moduli at most $x$ for a fixed constant $D$ and all large $x$. As the write-up describes it, the construction avoids the usual primorial axis of classes on products of all small primes: it fixes base prime coordinates and a closing prime, assigns the nonzero residues of each late coordinate injectively to sparse supports consisting of a pair of earlier coordinates, reserves private singletons so that every class has an integer only it covers, which is minimality, and transports the frame to integer congruences by the Chinese remainder theorem; the free choice of the injection at each coordinate gives the count. The estimate fixes the scale of $\log\log F$ only: the bundle's two bounds pin $\log F(x)$ between $x/(\log x)^{4+o(1)}$ and $O(x\log x)$, so the order of $\log F$, not only its constant, is open; the write-up's remark that sharper asymptotics such as the constant in $\log F(x)\asymp x\log x$ remain open presupposes an order the bounds do not establish. Against the site's commentary, which records the lower bound $F(x)\ge\exp((\log x)^{3-o(1)})$ from the construction of Balister, Bollobás, Morris, Sahasrabudhe and Tiba, the claim places $F$ near the trivial upper bound. The expectation of very slow growth that the commentary attributes to Erdős concerned a different quantity, the number $j_x$ of covering systems with moduli distinct across systems and below $x$ (survey of 1980, printed p. 95), which Hough's theorem bounds, as the Formulation paragraph of the problem page records; the claim does not contradict it. The bundle linked above holds a Lean 4 project (toolchain v4.31.0, pinned Mathlib) whose final theorem erdos1188_loglog_ratio_tendsto_one states the limit for a counting function coveringCount that filters the power set of all canonical classes with moduli in $[2,x]$ by distinct moduli, covering every integer and no proper subfamily covering; its entry is dated 2026-07-12. The write-up reports a sorry-free build with axioms propext, Classical.choice and Quot.sound, an independent exact checker for a 70-class witness below modulus 1000, and a referee step inside the Star Fleet Math system that rejected an earlier, weaker squarefree construction and audited the definition against the problem statement. The bundle's record entry is dated 2026-07-12, and Star Fleet Math's listing data record the result's acceptance at 15:37 UTC that day, which gives the page its date; the solution page shows no date. The site's proof-claims tab carries the claim, submitted at 01:59 UTC on 2026-07-15 by Colin Snyder (the forum user coffeewithcolin) and credited to GPT 5.6 in a custom harness. Star Fleet Math 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.

Submission note. Posted to erdosproblems.com as a proof claim by Colin Snyder (account coffeewithcolin) on 15 July 2026, giving "GPT 5.6 (custom harness)" as the AI used:

We claim $F(x)=\exp\left(x^{1+o(1)}\right)$: formally, $\log\log F(x)/\log x\to 1$ (Lean theorem erdos1188_loglog_ratio_tendsto_one). So the count of minimal distinct covering systems is nearly doubly exponential, against the reported expectation of slow growth. Proved in Lean 4 / Mathlib, standard axioms only, no sorry. Idea: the upper bound is easy (at most one residue per modulus gives $\exp(O(x\log x))$); the problem lives in the lower bound, which needs enormously many genuinely distinct MINIMAL systems with bounded moduli. The construction drops the classical rigid "primorial axis" entirely: base CRT prime coordinates plus a closing prime, where each late coordinate's residues are assigned injectively to sparse cross-pair supports, and reserved private singletons give every congruence its own witness integer, which is exactly minimality. Notes: An earlier squarefree construction gave a weaker lower scale and was rejected by our own independent review precisely because the bounds did not meet; the accepted proof closes the gap. Verify: unzip, build, then "#print axioms erdos1188_loglog_ratio_tendsto_one" gives exactly [propext, Classical.choice, Quot.sound], no sorry in sources.

Depends on. Nothing in this wiki.

Standing. Claimed: no journal publication, referee report, curator acceptance or outside review is recorded through 2026-10-06; the referee named in the write-up, 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 17 April 2026). The formal-conjectures statement file ErdosProblems/1188.lean, at its commit of 2026-09-18, tags the problem research solved with a formal_proof attribute pointing to the copy of this Lean proof hosted in Will Blair's lean-proofs repository at the commit of 2026-07-30 linked above, under starfleet/erdos-1188, whose final theorem erdos1188_loglog_ratio_tendsto_one matches the bundle's; the repository's main branch no longer holds that tree (as of 2026-10-07). The Lean project is described, not built, replayed or audited by this corpus, so it is not counted as evidence, and no formalized evidence is listed.