Skip to content

Erdős problem 205

Is it true that all sufficiently large nn can be written as 2k+m2^k+m for some k≥0k\geq 0, where Ω(m)<log⁡log⁡m\Omega(m)<\log\log m? (Here Ω(m)\Omega(m) is the number of prime divisors of mm counted with multiplicity.)

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/205.lean

Formal Conjectures

FormalConjectures/ErdosProblems/205.leanErdos205.erdos_205.parts.i1 lineExact file
False ↔ ∀ᶠ (n : ℕ) in Filter.atTop, Erdos205.IsRepresentable (fun m => Real.log (Real.log ↑m)) n
SolvedStatement only, no proof

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:205
  • PLBY Lean proofsErdosProblems.Erdos205

Reported activity

Reported by these sources. Not reviewed here.

Continue