Skip to content

Erdős problem 355

Is there a lacunary sequence A⊆NA\subseteq \mathbb{N} (so that A={a1<⋯ }A=\{a_1 < \cdots\} and there exists some λ>1\lambda > 1 such that an+1/an≥λa_{n+1}/a_n\geq \lambda for all n≥1n\geq 1) such that {∑a∈A′1a:A′⊆A finite}\left\{ \sum_{a\in A'}\frac{1}{a} : A'\subseteq A\textrm{ finite}\right\} contain all rationals in some open interval?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/355.lean

Formal Conjectures

FormalConjectures/ErdosProblems/355.leanErdos355.erdos_3554 linesExact file
True ↔  ∃ A,    IsLacunary A ∧      ∃ u v, u < v ∧ ∀ (q : ℚ), ↑q ∈ Set.Ioo u v → q ∈ {x | ∃ A', ∃ (_ : ↑A' ⊆ Set.range A), ∑ a ∈ A', 1 / ↑a = x}
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:355
  • PLBY Lean proofsErdosProblems.Erdos355

Reported activity

Reported by these sources. Not reviewed here.

  • Formalization

    Erdős AI contributions wiki · 30 Jan-13 Mar, 2026

    Machine
    Aristotle, Gemini 3
    Open the source record

Continue