Skip to content

Erdős problem 202

Let n1<⋯<nr≤Nn_1<\cdots < n_r\leq N with associated ai(modni)a_i\pmod{n_i} such that the congruence classes are disjoint (that is, every integer is ≡ai(modni)\equiv a_i\pmod{n_i} for at most one 1≤i≤r1\leq i\leq r). How large can rr be in terms of NN?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/202.lean

Formal Conjectures

FormalConjectures/ErdosProblems/202.leanErdos202.erdos_2021 lineExact file
∃ 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:202
  • PLBY Lean proofsErdosProblems.Erdos202

Reported activity

Work these sources record against this Problem. Source-reported attribution, 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

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page