Skip to content

Erdős problem 464

Let A={n1<n2<⋯ }⊂NA=\{n_1<n_2<\cdots\}\subset \mathbb{N} be a lacunary sequence (so there exists some ϵ>0\epsilon>0 with nk+1≥(1+ϵ)nkn_{k+1}\geq (1+\epsilon)n_k for all kk). Must there exist an irrational θ\theta such that {∥θnk∥:k≥1}\{ \|\theta n_k\| : k\geq 1\} is not dense in [0,1][0,1] (where ∥x∥\| x\| is the distance to the nearest integer)?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/464.lean

Formal Conjectures

FormalConjectures/ErdosProblems/464.leanErdos464.erdos_4643 linesExact file
True ↔  ∀ (n : ℕ → ℕ),    StrictMono n → (∀ (k : ℕ), 0 < n k) → IsLacunary n → ∃ θ, Irrational θ ∧ ¬Dense (Set.range fun k => ↑(θ * ↑(n k)))
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:464

Reported activity

Reported by these sources. Not reviewed here.

Continue