Erdős problem 825

Is there an absolute constant $C > 0$ such that every integer $n$ with $\sigma(n) > Cn$ is the distinct sum of proper divisors of $n$ ?

Sources

The source's own material, retained exactly.

2 retained statements36c6d0fef71a

FormalConjectures/ErdosProblems/

825.lean

Retained formal statement2 of 2

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$ .

FormalConjectures/ErdosProblems/825.leanErdos825.erdos_825.variants.necessary_cond2 linesExact file

1∀ (C : ℝ),2  0 < C → (∀ (n : ℕ), ↑((ArithmeticFunction.sigma 1) n) > C * ↑n → ∃ s ⊆ n.properDivisors, n = s.sum id) → 2 < C

SolvedStatement only, no proof