Combinatorics

Erdős 236

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)

References

erdosproblems.com/236

No one has attempted this yet.

Formal statement

Lean type

(fun n => ↑(Erdos236.f n)) =o[Filter.atTop] fun n => Real.log ↑n

What you must prove

import FormalConjectures.ErdosProblems.«236»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos236.erdos_236" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/236.lean

Source type SHA-256: sha256:b364b1aa2fb7181e7c8139c6133d3eb644e83ab723524c0f8dbe8d5de7fd430a
Task id: fc-379fc029-erdos236-erdos-236-2149496ce2-formalized-v1
Task commitment: sha256:78ff51e3a4a8508112aaa59b11663d0de75662c9fe67fcbcdd23238c305aceaf

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.