Skip to content

Erdős problem 25

Let n1<n2<…n_1 < n_2 < \dots be an arbitrary sequence of integers, each with an associated residue class ai(modni)a_i \pmod{n_i}. Let AA be the set of integers nn such that for every ii either n<nin < n_i or n≢ai(modni)n \not\equiv a_i \pmod{n_i}. Must the logarithmic density of AA exist?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/25.lean

Formal Conjectures

FormalConjectures/ErdosProblems/25.leanErdos25.erdos_254 linesExact file
True ↔  ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ),    (∀ (i : ℕ), 0 < seq_n i) →      StrictMono seq_n → ∃ d, {x | ∀ (i : ℕ), ↑x < ↑(seq_n i) ∨ ¬↑x ≡ seq_a i [ZMOD ↑(seq_n i)]}.HasLogDensity d
OpenStatement only, no proof

Reported activity

Reported by these sources. Not reviewed here.

  • AI collaborating with humans

    Erdős AI contributions wiki · 19 Mar, 2026

    Machine
    GPT-5.4 Pro
    People
    Przemek Chojecki
    Open the source record

Continue