Let $A \subseteq N$ be such that $∣ A \cap [1, 2 x]∣ - ∣ A \cap [1, x]∣ \to \infty as x \to \infty$ and $n \in A \sum {θ n} = \infty$ for every $θ \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$ .

Open — best to date is a honest null, not yet sealed.

number theory · open · formalized (Lean) · 1 attempt

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

evidence

honest null

needs verification

attempted via frontier 'sidon/B2' (transfer_strength=none) -> no_progress

No solve/partial on this pass. Transfer into the owned frontier was 'none'. Do not re-attack cold; needs a new idea or richer accumulated context.

unverified AI candidates (2)

gpt-erdos · GPT-5.2 Pro + Deep Research · unverified

What you wrote is **an open Erdős problem** about “complete” sets (meaning: all large integers can be written as a sum of **distinct** elements of the set). As far as the current literature summary on this problem goes, **no full proof is known** in the exact form you stated. ([Erdős Problems][1])

candidate solution ↗

llm-hunter · gpt pro 5.2 · unverified

1 LLM attack(s) recorded (gpt pro 5.2); unverified.

candidate solution ↗

formal

AMS 11 · open (literature)

theorem erdos_254 :
    ∀ (A : Set ℕ),
      (Tendsto (fun x : ℕ ↦ (A ∩ Icc 1 (2 * x)).ncard - (A ∩ Icc 1 x).ncard) atTop atTop) ∧
      (∀ θ : ℝ, 0 < θ → θ < 1 → ¬ Summable (fun n : A ↦ distToNearestInt (θ * (n : ℝ)))) →
        ∀ᶠ m in atTop, IsSumOfDistinct A m

formal-conjectures/254.lean ↗

status

open

evidence

formal

status

Search Vela