Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.

Updated Oct 8

Problem 202

claims/: The 6 claim pages of Problem 202, one per claimant's result; the problem's standing derives from them.

Statement. Let $n_1<\cdots < n_r\leq N$ with associated $a_i\pmod{n_i}$ such that the congruence classes are disjoint (that is, every integer is $\equiv a_i\pmod{n_i}$ for at most one $1\leq i\leq r$ ). How large can $r$ be in terms of $N$ ?

Formulation. The moduli are positive integers, so $1\le n_1<\cdots<n_r\le N$ for a positive integer $N$ . Write $f(N)$ for the maximum possible $r$ , as the site's commentary does. This maximum exists because the modulus sets and their residue assignments form a finite collection. Maximum cardinality differs from mere inclusion-maximality: the single class modulo $1$ cannot be extended, but for $N\ge4$ the classes $0\pmod2$ and $1\pmod4$ give a larger family. Restricting moduli to be at least $2$ gives the same $f(N)$ for $N\ge2$ .

Status. SOLVED (LEAN). The answer is known at the sharp logarithmic scale. Put $S(N)=\sqrt{\log N\log\log N}$ for $N>e$ , using natural logarithms. Then

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

Precisely, for every real $\eta>0$ there is $N_0(\eta)$ such that every integer $N\ge N_0(\eta)$ satisfies

N e^{-(1+\eta)S(N)}\le f(N)\le N e^{-(1-\eta)S(N)}.

This identifies the leading coefficient in the exponent. It does not assert $f(N)\sim N e^{-S(N)}$ or an exact formula at every finite $N$ . The ordinary proof is Ho's Theorem 1.1. The public formalization and verification evidence are described below, and the acceptance evidence is recorded on Ho's claim page.

Source. erdosproblems.com/202, accessed 2026-09-05. Cite as: T. F. Bloom, Erdős Problem #202, https://www.erdosproblems.com/202.

References.

[BFV13] de la Bretèche, Régis and Ford, Kevin and Vandehey, Joseph, On non-intersecting arithmetic progressions. Acta Arith. (2013), 381-392.
[Ch05] Chen, Yong-Gao, On disjoint arithmetic progressions. Acta Arith. (2005), 143-148.
[Cr03b] Croot, III, Ernest S., On non-intersecting arithmetic progressions. Acta Arith. (2003), 233-238.
[ErSz68] Erdős, P. and Szemerédi, E., On a problem of P. Erdős and S. Stein. Acta Arith. (1968), 85-90.
[PaPh24] Park, Jinyoung and Pham, Huy Tuan, A proof of the Kahn-Kalai conjecture. J. Amer. Math. Soc. (2024), 235-243.
[Ho26] Ho, Boon Suan, Non-intersecting arithmetic progressions via spread cores. Author manuscript (2026), selected 3 May PDF.

Formalization. See the "Formalization and verification scope" section below for the pinned public implementations and recorded verification limits.

Current assessment

The complete ordinary Ho deductions, their BFV inputs, and the general Park–Pham threshold proof are compiled at their canonical source pages as author-recorded proof coverage at the explicitly stated classical inputs. Ho imports Park–Pham as a theorem; its full proof is located once at its own source. Ho does not assume the stronger BFV popular-core conjecture or the full sunflower conjecture. BFV's separate unresolved sunflower-corollary reconstruction is not an input to this solution. The sharp answer also yields the reciprocal-sum estimate in Problem 1190.

The primary source is Boon Suan Ho's nine-page manuscript, Non-intersecting arithmetic progressions via spread cores. The selected 3 May 2026 PDF is pinned in the source digest. Its first public PDF commit and announcement are dated 23 April 2026. The PDF names Ho and discloses substantial GPT-5.4 Pro participation, with iterative guidance and revision by Ho and Ho's responsibility for the final text. It does not identify a journal publication or referee acceptance.

The dated public discussion records the announcement and, on 14 May 2026, the proof implementation and Nat Sothanaphan's confirmation of both this formalization and that of Problem 1190, including formalization of the Park–Pham input. The community ledger (last revision, data) also records the full solution and the 14 May formalization, and lists as a candidate full solution the ULAM draft of 30 April 2026 credited to GPT-5.5 Pro, which claims the same asymptotic by a spread-core route and is recorded on its claim page. The site, labels the problem solved with a Lean qualification and records a last edit of 28 May. Thus the mathematical status rests on the primary proof and dated public verification evidence, beyond the site's status label. The targeted primary-source search through 5 September 2026 found no later contradiction or stronger quantitative answer; it is not an exhaustive search of unpublished claims.

Known results and proof route

Erdős and Stein conjectured $f(N)=o(N)$ , proved by Erdős–Szemerédi (1968) (claim page, accepted on the refereed paper). Subsequent bounds determine progressively sharper coefficients on the scale $S(N)$ ; each refereed bound has its own accepted partial claim page, linked in the table. In the following table, coefficients $(a,b)$ mean that for every $\eta>0$ , for all sufficiently large $N$ ,

N e^{-(a+\eta)S(N)}\le f(N)\le N e^{-(b-\eta)S(N)}.

Source	Lower coefficient $a$	Upper coefficient $b$
Croot (2003) (claim page)	$\sqrt2$	$1/6$
Chen (2005) (claim page)	No new lower bound	$1/2$
de la Bretèche–Ford–Vandehey (2013) (claim page)	$1$	$\sqrt3/2$
Ho (2026) (claim page)	$1$	$1$

The Croot and Chen entries above concern arbitrary distinct moduli. Croot's separate squarefree upper bound already had coefficient $1/2$ ; Chen removed that restriction. BFV conjectured that their lower coefficient $1$ was sharp.

Ho retains BFV's lower construction and uniform pruning argument. After pruning, the moduli have a common integer prime count $K\le3\sqrt{\log N/\log\log N}$ and distinct squarefree kernels. The spread-disjointness deduction from the published Park–Pham theorem gives a dense core with loss $(C_0\log(eK))^{|C|}$ . Its accumulated contribution in the descending chain is $o(\log N)$ , allowing the final coefficient $1$ .

Structure of large families

Fornal–Sun's July 2026 preprint gives a further structural consequence for every family of maximum cardinality $f(N)$ . For all sufficiently large $N$ , it contains distinct moduli $q,q'$ such that, with $g=\gcd(q,q')$ ,

g\ge N\exp\bigl(-(1+o(1))S(N)\bigr),\qquad \max\{q/g,q'/g\}\le\exp\bigl((1+o(1))S(N)\bigr).

Both bounds hold for the same pair, and its two quotients are coprime. This follows from their Corollary 1.2 and Ho's cardinality theorem. It adds information about the moduli inside an extremal family without changing the counting asymptotic or the status of this problem. The source digest records the selected arXiv v1 and the scope of its proof review.

Formalization and verification scope

The actual P202 implementation is pinned to the Shashi development of 14 May 2026. Its bundled mathematical PDF is byte-identical to the selected Ho source. The definitions of finite admissibility and maximum cardinality, and the main theorem's all-positive-error eventual quantifiers, match the statement above. A lexical scan outside comments found no sorry or admit tokens in that implementation; this is a static check, not evidence of elaboration or kernel acceptance.

The adaptation in Boris Alexeev's lean-proofs repository credits formalization to Pawan Sasanka Ammanamanchi and Claude. It ports the same development. The original formal-conjectures statement link is retained; its revision of 2026-09-04 contains statement scaffolding and links to the actual proof, rather than supplying a complete implementation in that file.

This corpus has not built or audited either development, so it gives no formalized evidence. Exact source, code, signature, and snapshot pins, with the detailed boundaries, are recorded in the Ho source's source card.

Linked library material

These entries are derived from explicit links on library pages. They are navigation only and do not by themselves record mathematical progress.

Linked from (61)

Erdős and Szemerédi's proof that f(N)=o(N)Croot's bounds with coefficients square root of 2 and one sixth Chen's upper bound with coefficient one half De la Bretèche, Ford and Vandehey's bounds with coefficients 1 and root 3 over 2 Ho's sharp asymptotic for disjoint residue classes The ULAM draft's spread-core upper bound for disjoint residue classes problems/covering_systems/E0202/claims Problem 1190 Zribi's conditional transfer from the Problem 202 asymptotic The ULAM draft's unconditional route to the reciprocal-sum asymptotic Covering Systems covering_systems/chen_2005_disjoint_arithmetic_progressions Theorem — Chen’s unrestricted half-constant upper bound On non-intersecting arithmetic progressions Upper bound without the squarefree restriction Smooth-number input at the square-root logarithmic scale Few integers have many distinct prime factors A disjoint family from ordered prime-power factors Selecting common small primes until a large prime is frequent Excluding large prime powers from smooth integers Upper bound for disjoint progressions with squarefree moduli On non-intersecting arithmetic progressions Conjecture 1 — the coefficient-one endpoint in the 2013 paper The lower construction in Theorem 1 Section 4.1 — uniform pruning of an extremal progression family Theorem 1 — the original unconditional disjoint-progression bounds On a problem of P. Erdős and S. Stein The original prime-chain lower construction Theorem 1 — the original density-zero bound for disjoint progressions On the problem of large gcd for disjoint residue classes A large common divisor in a nearly largest progression family Exact external inputs and background boundaries The gcd graph and normalized maximal-divisor weights Counting the prime-profile partition classes A Rankin bound with prescribed prime-box multiplicities Exceptional vertices and weights in the gcd graph Möbius-weighted Fourier positivity A partition with small within-class gcd sums The weighted estimate for an arbitrary partition An alternative factor-exponent partition A nearly linear gcd among disjoint residue classes Non-intersecting arithmetic progressions via spread cores A dense core in an intersecting uniform family Compatibility of two integer residue classes Uniform counting after removing fixed prime supports Weighted pigeonholing over a nonempty finite index set Spread families contain disjoint members The BFV pruning input in Ho's notation The descending chain of exact prime-power blocks The sharp logarithmic scale for non-intersecting progressions

Graph