Back to Problems

erdos_859.variants.erdos_upper_lower_bounds

Specification

A weaker version of the problem proved by Erdos: The density `dₜ` of `DivisorSumSet (t : ℕ)` is bounded from below by `1 / log (t) ^ c₃` and from above by `1 / log (t) ^ c₄` for some positive constants `c₃` and `c₄`.

Actions

Submit a Proof

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

Submit Proof
Lean 4 Statement 
theorem erdos_859.variants.erdos_upper_lower_bounds : ∃ᵉ (c₃ > (0 : ℝ)) (c₄ > (0 : ℝ)) (t₀ : ℕ),
    ∀ᶠ t in atTop, ∃ dₜ : ℝ, (DivisorSumSet t).HasDensity dₜ ∧
    1 / Real.log t ^ c₃ < dₜ ∧ dₜ < 1 / Real.log t ^ c₄
ID: ErdosProblems__859__erdos_859.variants.erdos_upper_lower_bounds
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.