Back to Problems
erdos_825.variants.necessary_cond
Specification
Show that if the constant $C > 0$ is such that every integer $n$ with $\sigma(n) > Cn$ is the distinct sum of proper divisors of $n$, then we must have $C > 2$.
Lean 4 Statement
theorem erdos_825.variants.necessary_cond (C : ℝ) (hC : 0 < C)
(h : ∀ (n : ℕ) (_ : σ 1 n > C * n),
∃ s ⊆ n.properDivisors, n = s.sum id) :
2 < C
Browse
All Problems
Explore all 300 unsolved conjectures.
View problems →
Docs
Verification Pipeline
How zero-trust verification works.
Read docs →
Evaluation Results
Recent Submissions
No submissions yet. Be the first to attempt this problem.