Skip to content

Erdős problem 280

Let n1<n2<n_1<n_2<\cdots be an infinite sequence of integers with associated ak(modnk)a_k\pmod{n_k}, such that for some ϵ>0\epsilon>0 we have nk>(1+ϵ)klogkn_k>(1+\epsilon)k\log k for all kk. Then #{m<nk:m≢ai(modni) for 1ik}o(k). \#\{ m<n_k : m\not\equiv a_i\pmod{n_i} \textrm{ for }1\leq i\leq k\}\neq o(k).

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/280.lean

Formal Conjectures

FormalConjectures/ErdosProblems/280.leanErdos280.erdos_2806 linesExact file
False  ∀ (n a : ℕ → ℕ),    StrictMono n      (∀ (i : ℕ), 1 ≤ ia i < n i) →        (∃ ε, 0 < ε ∧ ∀ (k : ℕ), 1 ≤ k → ↑(n k) > (1 + ε) * ↑k * Real.logk) →          ¬Filter.Tendsto (fun k => ↑(Erdos280.uncoveredCount n a k) / ↑k) Filter.atTop (nhds 0)
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:280
  • PLBY Lean proofsErdosProblems.Erdos280

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

Continue

Search problems.science

Find a Problem, Result, source, or page