Erdős Problem 236

Reference: erdosproblems.com/236

theorem Erdos236.erdos_236 : (fun (n : ℕ) => ↑(Erdos236.f✝ n)) =o[Filter.atTop] fun (n : ℕ) => Real.log ↑n

Let $f(n)$ count the number of solutions to $n=p+2^k$ for prime $p$ and $k\geq 0$. Show that $f(n)=o(\log n)$.