Erdős problem 202

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$ ?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

FormalConjectures/ErdosProblems/202.lean

Formal Conjectures

FormalConjectures/ErdosProblems/202.leanErdos202.erdos_2021 lineExact file

1∃ o, o =o[Filter.atTop] 1 ∧ ∀ᶠ (N : ℕ) in Filter.atTop, ↑(Erdos202.f N) = ↑N * scaleL N ^ (-1 + o N)

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Reported by these sources. Not reviewed here.

AI collaborating with humans
Erdős AI contributions wiki · 23 Apr, 2026
Machine
GPT-5.4 Pro
People
Boon Suan Ho
Open the source record
Formalization
Erdős AI contributions wiki · 14 May, 2026
Machine
Unspecified
Open the source record
AI collaborating with humans
Erdős AI contributions wiki · 30 Apr, 2026
Machine
GPT-5.5 Pro
People
Przemek Chojecki
Open the source record
argument
VibeMathed
Machine
GPT-5.4 Pro
People
Boon Suan Ho
Reported outcome
resolved
Open the source record