Back to Problems

erdos_341

Specification

Let $A=\{a_1 < \cdots < a_k\}$ be a finite set of integers and extend it to an infinite sequence $\overline{A}=\{a_1 < a_2 < \cdots \}$ by defining $a_{n+1}$ for $n \geq k$ to be the least integer exceeding $a_n$ which is not of the form $a_i + a_j$ with $i,j \leq n$. Is it true that the sequence of differences $a_{m+1}-a_m$ is eventually periodic? This problem is discussed under Problem 7 on Green's open problems list.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement
theorem erdos_341 :
    answer(sorry) ↔
      ∀ (a : ℕ → ℤ),
        (∀ᶠ n in atTop,
          IsLeast { x | a n < x ∧ x ∉ { a i + a j | (i ≤ n) (j ≤ n) } } (a (n + 1))) →
        let d
ID: ErdosProblems__341__erdos_341
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.