Skip to content

Erdős problem 347

Is there a sequence A={a1≤a2≤⋯ }A=\{a_1\leq a_2\leq \cdots\} of integers with lim⁡an+1an=2\lim \frac{a_{n+1}}{a_n}=2 such that P(A′)={∑n∈Bn:B⊆A′ finite }P(A')= \left\{\sum_{n\in B}n : B\subseteq A'\textrm{ finite }\right\} has density 11 for every cofinite subsequence A′A' of AA?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

347.lean

Retained formal statement1 of 1

Is there a sequence A={a1≤a2≤⋯ }A=\{a_1\leq a_2\leq \cdots\} of integers with lim⁡an+1an=2\lim \frac{a_{n+1}}{a_n}=2 such that P(A′)={∑n∈Bn:B⊆A′ finite }P(A')= \left\{\sum_{n\in B}n : B\subseteq A'\textrm{ finite }\right\} has density 11 for every cofinite subsequence A′A' of AA?

This has been solved in the affirmative by ebarschkis in the comments (based on idea of Tao and van Doorn, also in the comments).

This was formalized in Lean by Barschkis using Aristotle.

FormalConjectures/ErdosProblems/347.leanErdos347.erdos_3475 linesExact file
True ↔  ∃ a,    Monotone a ∧      Filter.Tendsto (fun n => ↑(a (n + 1)) / ↑(a n)) Filter.atTop (nhds 2) ∧        ∀ (ι : ℕ → ℕ), (Set.range ι)ᶜ.Finite → (subsetSums (Set.range (a ∘ ι))).HasDensity 1
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