---

Claim. For an integer $m\ge1$ let $\epsilon_m$ be the supremum of $\sum_i1/n_i$ over finite families of distinct moduli $m<n_1<\cdots<n_k$ admitting pairwise disjoint residue classes $a_i\pmod{n_i}$. With $S(m)=\sqrt{\log m\log\log m}$ in natural logarithms,

$$\epsilon_m=\exp\bigl(-(1+o(1))S(m)\bigr),$$

that is, for every $\eta>0$ and all large $m$, $e^{-(1+\eta)S(m)}\le\epsilon_m\le e^{-(1-\eta)S(m)}$. This is Corollary 1.2 of Ho's nine-page manuscript, the library's Ho 2026, with the statement and its deduction compiled on its Corollary 1.2 page. The deduction is the transfer from the sharp asymptotic for the largest number $f(N)$ of disjoint classes with distinct moduli at most $N$: the upper bound by partial summation of $A(t)\le f(t)$ for a family's counting function against $t^{-2}$, with a tail-integral lemma uniform over finite families; the lower bound by taking an extremal family for $f(N)$ at $N=\lceil me^{2S(m)}\rceil$ and deleting its at most $m$ moduli not exceeding $m$. The manuscript's final page discloses substantial mathematical and expository contributions from GPT-5.4 Pro under Ho's guidance and revision, with Ho responsible for the text; the site credits the resolution of Problem 202 to GPT-5.4 Pro and derives this estimate from it. The first public posting and announcement are dated 2026-04-23, which names the page; the PDF cited is the 3 May 2026 commit linked above. The estimate determines the leading exponent only: it does not give $\epsilon_m\sim e^{-S(m)}$ or a value at any finite cutoff.

This is the corrected Statement of Problem 1190, whose supremum replaces the site's maximum; Ho, the site's commentary and both Lean developments use the same supremum, and the problem page's Notes record that no finite family attains it.

Depends on. Ho's sharp asymptotic for Problem 202, the theorem $f(N)=N\exp(-(1+o(1))S(N))$ whose upper bound is the new content and whose lower bound is the construction of de la Bretèche, Ford and Vandehey; the transfer itself uses only that asymptotic, partial summation and the stability of $S$ under the change of scale.

Acceptance. Reviewed: Ho announced the manuscript, which states and proves this corollary beside the Problem 202 theorem, on the site's Problem 202 thread on 2026-04-23, where the site's curator (T. F. Bloom) replied that they would update the site once a formalization was provided or a human had vouched for the proof; on 2026-05-14 a Lean 4 development formalizing Theorem 1.1 and Corollary 1.2 was posted there. It reported that its Problem 202 theorem depends only on propext, Classical.choice and Quot.sound and had passed a SafeVerify check, and that the 1190 corollary uses no further axioms. Nat Sothanaphan confirmed it the same day, adding that the Park–Pham input was formalized rather than assumed; the site labels this problem SOLVED (LEAN) and states in its commentary that the resolution of Problem 202 implies $\epsilon_m=L(m)^{-1+o(1)}$ by the same reduction (page last edited 2026-05-28, as of 2026-10-07), and the community ledger of AI contributions records the solution and the formalization. Not refereed: the manuscript is an author PDF with no journal publication or referee report located through 2026-09-05. Not counted as formalized: the linked development defines $\epsilon_m$ as an sSup of reciprocal sums of finite admissible families and its main theorem states the eventual two-sided bound above, with no sorry or admit token outside comments, but this corpus has run no Lean build, kernel replay or axiom audit of it and records no CI result for the pinned revision; Boris Alexeev's lean-proofs adaptation linked above ports the same development. The problem page's section on formalization and verification scope and the source card record the exact pins and limits.

Not covered. The second-order behavior of $\epsilon_m$, including whether $\epsilon_m\sim e^{-S(m)}$. Two contemporary accounts of the same estimate have their own pages: Zribi's conditional note and the ULAM draft.