Conjectures.io

Number theory

Erdős 357 - infinite set sum

Suppose AA is an infinite set such that all finite sums of consecutive terms of AA are distinct. Then it is conjectured that the sum ∑k1ak\sum_k \frac{1}{a_k} converges.

References

No one has attempted this yet.

Formal statement

Lean type

∀ (A : ℕ → ℕ), StrictMono A → Erdos357.HasDistinctSums A → Summable fun i => 1 / ↑(A i)

What you must prove

import FormalConjectures.ErdosProblems.«357»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos357.erdos_357.variants.infinite_set_sum" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/357.lean

Source type SHA-256
sha256:873d61e456eb854ca539c5c628143c137e5fca4a744f800836ee63bdd7f3d19d
Task id
fc-379fc029-variants-infinite-set-sum-fa4ea97ef1-formalized-v1
Task commitment
sha256:174fae54978f9759eb4019822f69c5be2af7e88fe9d95c5eefac97214c39a3c0

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.