Erdős Problem 236

Reference: erdosproblems.com/236

def Erdos236.f (n : ℕ) : ℕ

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

Equations

• Erdos236.f n = (List.filter (fun (k : ℕ) => decide (Nat.Prime (n - 2 ^ k))) (List.range (n.log2 + 1))).length

theorem Erdos236.erdos_236 : (fun (n : ℕ) => ↑(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)$.