Erdős Problem 236

Conjecture 236 · Erdős

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)$ .

Formal statement · Lean 4.lean

theorem erdos_236: (fun n => (f n : ℝ)) =o[atTop] (fun n => Real.log (n : ℝ)) := by
  sorry

Proof. sorry

Nobody has tried yet.