Let $1 \leq a_{1} < a_{2} < \dots$ be an infinite sequence of integers such that $a_{i + 1} / a_{i} \to 1$ . If every infinite arithmetic progression contains infinitely many integers which are the sum of distinct $a_{i}$ then every sufficiently large integer is the sum of distinct $a_{i}$ .

Worked, still open.

number theory · solved · formalized (Lean) · 0 attempts

use this record

vela registry pull vfr_37aec80d874a0239

vela reproduce examples/erdos-problems

formal

AMS 11 · solved (literature)

theorem erdos_253 : ¬ ∀ a : ℕ → ℕ, 0 < a 0 →
    RepresentsAPs a → (Filter.atTop.Tendsto (fun n ↦ (a <| n + 1 : ℝ) / a n) (𝓝 1)) →
      subsetSums (Set.range a) ∈ Filter.cofinite

formal-conjectures/253.lean ↗

status

solved

formal

status

Search Vela