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?

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/254.lean

Formal Conjectures

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.

Proof manifests naming this Problem

  • William Blair Lean proofswilliamjblair:Erdos254.erdos_254

Reported activity

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

  • argument

    VibeMathed

    Machine
    GPT-5.6 starships (Claude Fable 5 reviewer)
    Reported outcome
    candidate
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page