Skip to content

Erdős problem 254

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

Sources

The source's own material, retained exactly.

4 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

254.lean

Retained formal statement1 of 3

Let A⊆NA\subseteq \mathbb{N} be such that ∣A∩[1,2x]∣−∣A∩[1,x]∣→∞ as x→∞\lvert A\cap [1,2x]\rvert -\lvert A\cap [1,x]\rvert \to \infty\textrm{ as }x\to \infty and ∑n∈A{θn}=∞\sum_{n\in A} \{ \theta n\}=\infty for every θ∈(0,1)\theta\in (0,1), where {x}\{x\} is the distance of xx from the nearest integer. Then every sufficiently large integer is the sum of distinct elements of AA.

FormalConjectures/ErdosProblems/254.leanErdos254.erdos_2544 linesExact file
∀ (A : Set ℕ),  (Filter.Tendsto (fun x => (A ∩ Set.Icc 1 (2 * x)).ncard - (A ∩ Set.Icc 1 x).ncard) Filter.atTop Filter.atTop ∧      ∀ (θ : ℝ), 0 < θ → θ < 1 → ¬Summable fun n => distToNearestInt (θ * ↑↑n)) →    ∀ᶠ (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.