Skip to content

Erdős problem 355

Is there a lacunary sequence ANA\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 n1n\geq 1) such that {aA1a:AA 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
TrueA,    IsLacunary Au v, u < v ∧ ∀ (q : ℚ), ↑qSet.Ioo u vq ∈ {x | ∃ A', ∃ (_ : ↑A'Set.range A), ∑ aA', 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

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

  • Formalization

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

    Machine
    Aristotle, Gemini 3
    Open the source record

Continue

Search problems.science

Find a Problem, Result, source, or page