Let $1 \leq n_{1} < n_{2} < \dots$ be an arbitrary sequence of integers, each with an associated residue class $a_{i} (mod n_{i})$ . Let $A$ be the set of integers $n$ such that for every $i$ either $n < n_{i}$ or $n \neq \equiv a_{i} (mod n_{i})$ . Must the logarithmic density of $A$ exist?

Worked, still open.

number theory · open · formalized (Lean) · 0 attempts

machinery: covering-system,prime-distribution,additive-combinatorics,Davenport-Erdos-logarithmic-density,set-of-multiples

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

No one currently knows in full generality.

candidate solution ↗

llm-hunter · gpt 5.2, gpt pro 5.2 · unverified

4 LLM attack(s) recorded (gpt 5.2, gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_25 : answer(sorry) ↔
    ∀ (seq_n : ℕ → ℕ) (seq_a : ℕ → ℤ), (∀ i, 0 < seq_n i) → StrictMono seq_n →
      ∃ d, Set.HasLogDensity
        { x : ℕ | ∀ i, (x : ℤ) < seq_n i ∨ ¬((x : ℤ) ≡ seq_a i [ZMOD seq_n i]) } d

formal-conjectures/25.lean ↗

status

open

evidence

formal

status

Search Vela