Formal target: Corpus.Erdos236.erdos_236

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

Exact formal statement

Asymptotics.IsLittleO.{0, 0, 0} Filter.atTop.{0} (fun n => Nat.cast.{0} (Corpus.Erdos236.f n)) fun n =>
  Real.log (Nat.cast.{0} n)

This target is a formal statement, not a proof of the problem.

Environment availability: available.