Erdős problem 357
Let be the maximal such that there exist integers such that all sums of the shape are distinct. It is known that . Source: See comment by Desmond Weisenberg here: https://www.erdosproblems.com/forum/thread/357.
Sources
FormalConjectures/ErdosProblems/
357.lean
Retained formal statement
Suppose is an infinite set such that all finite sums of consecutive terms of are distinct. Then it is conjectured that the sum converges.
∀ (A : ℕ → ℕ), StrictMono A → Erdos357.HasDistinctSums A → Summable fun i => 1 / ↑(A i)OpenStatement only, no proof