Combinatorics · Last catalog review 26 Jul 2026

Erdős Problem 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

Published 6 May 2026Never attempted

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-e923379e-erdos236-erdos-236-bb09909b42-formalized-v1
Task commitment: sha256:79f1a483309394a7a38b2a012c19f3563503901fd7dc0ce89ed92425f97c21e1

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.