---

Claim. Let $f(N)$ be the largest $r$ for which there are moduli $1\le n_1<\cdots<n_r\le N$ and residue classes $a_i\pmod{n_i}$ with no integer in two of the classes, the quantity asked for in Problem 202. Then, with $S(N)=\sqrt{\log N\log\log N}$,

$$f(N)=N\exp\bigl(-(1+o(1))S(N)\bigr),$$

that is, for every $\eta>0$ and all large $N$, $Ne^{-(1+\eta)S(N)}\le f(N)\le Ne^{-(1-\eta)S(N)}$. The lower bound is the construction of de la Bretèche, Ford and Vandehey, who conjectured that its coefficient $1$ is sharp; the new content is the matching upper bound. Ho keeps their pruning of an extremal family to moduli with a common prime count and distinct squarefree kernels, and replaces the minimal-family step of their descending-chain argument by a dense-core lemma derived from the Park–Pham expectation-threshold theorem (the former Kahn–Kalai conjecture): every nonempty intersecting family of distinct $k$-sets with $k\le K$ has a nonempty core contained in more than a $(C_0\log(eK))^{-|C|}$ share of its members. The accumulated loss along the chain is $o(\log N)$, which gives the coefficient $1$. The nine-page manuscript is compiled on the library card Ho 2026, whose Theorem 1.1 is this statement and whose result pages compile the whole deduction with its BFV and Park–Pham inputs at their own source pages. Its 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 proof to GPT-5.4 Pro prompted by Ho. The same argument gives the reciprocal-sum asymptotic of Problem 1190. The asymptotic identifies the leading coefficient in the exponent only; it does not give $f(N)\sim Ne^{-S(N)}$ or an exact value at any finite $N$.

Depends on. De la Bretèche, Ford and Vandehey's claim page, accepted: the lower bound is their construction, and Ho keeps their pruning of an extremal family. The Park–Pham theorem is compiled on its library page and is not a page of this wiki.

Acceptance. Reviewed: Ho announced the result on the site's discussion thread on 2026-04-23; the site's curator, Thomas F. Bloom, replied the same day promising to update the site once a formalization was provided or a human had vouched for the proof; on 2026-05-14 a Lean 4 formalization of the manuscript's Theorem 1.1 and Corollary 1.2 was posted on the thread, reporting that the main theorem depends only on propext, Classical.choice and Quot.sound and had passed a SafeVerify run, and Nat Sothanaphan confirmed it the same day, adding that the Park–Pham input was formalized rather than assumed; the site labels the problem solved with a Lean qualification and credits the proof in its commentary (page last edited 2026-05-28), and the community ledger of AI contributions, linked above at its last revision (data as of 30 June 2026), records the solution and the formalization. Not refereed: the manuscript is an author PDF on Ho's website with no journal publication or referee report located through 2026-09-05; the first public PDF and announcement are dated 2026-04-23, which gives the page its date, and the card compiles the 3 May 2026 commit linked above. Not counted as formalized: the linked Shashi development of 2026-05-14 bundles a PDF byte-identical to the 3 May 2026 PDF linked above, and its definitions and main theorem match the statement above, with no sorry or admit token outside comments; but this corpus has not built or audited the development, so the public confirmation is described and not counted. The adaptation in Boris Alexeev's lean-proofs repository, 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. A later claim of the same asymptotic, the ULAM draft of 2026-04-30 credited to GPT-5.5 Pro, has its own page and stays claimed.

Not covered. The second-order behavior of $f(N)$, including whether $f(N)\sim Ne^{-S(N)}$, and the structure of extremal families, on which Fornal and Sun's 2026 preprint is recorded on the problem page.