All open problems
Source labels openChecked July 26, 2026

Erdős ProblemsNumber theory

Erdős Problem 341

Let A={a1<<ak}A=\{a_1 < \cdots < a_k\} be a finite set of integers and extend it to an infinite sequence A={a1<a2<}\overline{A}=\{a_1 < a_2 < \cdots \} by defining an+1a_{n+1} for nkn \geq k to be the least integer exceeding ana_n which is not of the form ai+aja_i + a_j with $i...

Mathematical statement

Let A={a1<<ak}A=\{a_1 < \cdots < a_k\} be a finite set of integers and extend it to an infinite sequence A={a1<a2<}\overline{A}=\{a_1 < a_2 < \cdots \} by defining an+1a_{n+1} for nkn \geq k to be the least integer exceeding ana_n which is not of the form ai+aja_i + a_j with i,jni,j \leq n. Is it true that the sequence of differences am+1ama_{m+1}-a_m is eventually periodic?

This problem is discussed under Problem 7 on Green's open problems list.

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_341

Canonical source
Complete statement target, proof intentionally absentLean 4
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 := fun i  a (i + 1) - a i         p > 0, ᶠ m in atTop, d (m + p) = d m := by  sorry
Statement source
Formal Conjectures
Lean version
v4.27.0
Placeholder
Present; no proof artifact
Source evidence
Pinned source index
Fidelity review
Community formulation

References