Erdős problem 280 · problems.science

Let $n_1<n_2<\cdots$ be an infinite sequence of integers with associated $a_k\pmod{n_k}$ , such that for some $\epsilon>0$ we have $n_k>(1+\epsilon)k\log k$ for all $k$ . Then $\#\{ m<n_k : m\not\equiv a_i\pmod{n_i} \textrm{ for }1\leq i\leq k\}\neq o(k).$

Sources

Browse retained paths and inspect the exact material available for this Problem.

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

280.lean

Retained formal statement1 of 1

Cambie observed that this is false.

FormalConjectures/ErdosProblems/280.leanErdos280.erdos_2806 linesExact file

1False ↔2  ∀ (n a : ℕ → ℕ),3    StrictMono n →4      (∀ (i : ℕ), 1 ≤ i → a i < n i) →5        (∃ ε, 0 < ε ∧ ∀ (k : ℕ), 1 ≤ k → ↑(n k) > (1 + ε) * ↑k * Real.log ↑k) →6          ¬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.

Sources

Search problems.science