Erdős problem 254 · problems.science

If $A \subseteq \mathbb{N}$ has unbounded dyadic-shell counts and $\sum_{n \in A} \|\theta n\| = \infty$ for every $0 < \theta < 1$ , must $A$ be complete - is every sufficiently large integer a sum of distinct elements of $A$ ?

Sources

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

4 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

254.lean

Retained formal statement1 of 3

Let $A\subseteq \mathbb{N}$ be such that $\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert \to \infty\textrm{ as }x\to \infty$ and $\sum_{n\in A} \{ \theta n\}=\infty$ for every $\theta\in (0,1)$ , where $\{x\}$ is the distance of $x$ from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of $A$ .

FormalConjectures/ErdosProblems/254.leanErdos254.erdos_2544 linesExact file

1∀ (A : Set ℕ),2  (Filter.Tendsto (fun x => (A ∩ Set.Icc 1 (2 * x)).ncard - (A ∩ Set.Icc 1 x).ncard) Filter.atTop Filter.atTop ∧3      ∀ (θ : ℝ), 0 < θ → θ < 1 → ¬Summable fun n => distToNearestInt (θ * ↑↑n)) →4    ∀ᶠ (m : ℕ) in Filter.atTop, Erdos254.IsSumOfDistinct A m

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.

Sources

Search problems.science