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?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

355.lean

Retained formal statement1 of 1

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?

Bleicher and Erdős conjectured the answer is no.

In fact the answer is yes, with any lacunarity constant λ∈(1,2)\lambda\in (1,2) (though not λ=2\lambda=2), as proved by van Doorn and Kovač [DoKo25].

This was formalized in Lean by van Doorn using Aristotle.

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.

Search problems.science

Find a Problem, Result, source, or page