Erdős problem 825
Is there an absolute constant such that every integer with is the distinct sum of proper divisors of ?
Sources
FormalConjectures/ErdosProblems/
825.lean
Retained formal statement
Is there an absolute constant such that every integer with is the distinct sum of proper divisors of ?
This has been solved in the affirmative by Larsen - in fact, for any there exists such that if has only prime divisors and then is the distinct sum of proper divisors of .
True ↔ ∃ C, ∃ (_ : C > 0), ∀ (n : ℕ), ↑((ArithmeticFunction.sigma 1) n) > C * ↑n → ∃ s ⊆ n.properDivisors, n = s.sum idSolvedStatement only, no proof