Number theory
Erdős 357 - infinite set density
Suppose is an infinite set such that all finite sums of consecutive terms of are distinct. Then it is conjectured that has density 0.References
No one has attempted this yet.
Formal statement
Lean type
∀ (A : ℕ → ℕ), StrictMono A → Erdos357.HasDistinctSums A → (Set.range A).HasDensity 0What you must prove
import FormalConjectures.ErdosProblems.«357»
import TaskSupport
namespace Bounty
theorem target : fcTypeOfName% "Erdos357.erdos_357.variants.infinite_set_density" := by
sorry
end Bounty
Pinned source: FormalConjectures/ErdosProblems/357.lean
- Source type SHA-256
- sha256:3c615fd37ffe35e2505e2abad44f7b5b042c5625563adb5fda0e60f4caec8364
- Task id
- fc-379fc029-variants-infinite-set-density-20987dfd50-formalized-v1
- Task commitment
- sha256:674ddbfd8885dcdf5d07dbb8b39573165a2e6836791024d6c34d3a9041cdab5e
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.