Erdős Problem 358

Theorem 358 · Erdős

When $A_n = n$ , the function $f$ defined above counts the number of odd divisors of $n$ .

Formal statement · Lean 4.lean

theorem f_id : f id = fun n ↦ #{d ∈ n.divisors | Odd d} := by
  sorry

Proof. sorry

Nobody has tried yet.