Erdős Problem 277

Theorem 277 · Erdős

Is it true that, for every $c$ , there exists an $n$ such that $\sigma(n)>cn$ but there is no covering system whose moduli all divide $n$ ?

This was answered affirmatively by Haight [Ha79].

Formal statement · Lean 4.lean

theorem erdos_277 :
   answer(True) ↔ ∀ c : ℝ, ∃ n : ℕ, (σ 1 n : ℝ) > c * n ∧
      ∀ (m : StrictCoveringSystem ℤ), ∃ i, (n : ℤ) ∉ m.moduli i := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗