lean_workbook_plus_39881
ProvedLet be the number of positive divisors of the integer . An integer is called balanced if Prove there exist infinitely many balanced integers.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_39881 (d : ℕ → ℕ) (hd : d = fun k => (Nat.divisors k).card) : ∃ n, (d (n-1) ≤ d n ∧ d n ≤ d (n+1)) ∨ (d (n-1) ≥ d n ∧ d n ≥ d (n+1)) := by sorry
Source