Back to Problems

erdos_357.variants.infinite_set_lower_density

Specification

Suppose $A$ is an infinite set such that all finite sums of consecutive terms of $A$ are distinct. Then $A$ has lower density 0.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem erdos_357.variants.infinite_set_lower_density (A : ℕ → ℕ) (hA : StrictMono A)
    (hA : HasDistinctSums A) : (Set.range A).lowerDensity = 0
ID: ErdosProblems__357__erdos_357.variants.infinite_set_lower_density
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.