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.)

Sources

Browse retained paths and inspect the exact material available for this Problem.

5 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

205.lean

Retained formal statement2 of 5

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.) What about <ϵlog⁡log⁡m<\epsilon \log\log m?

Barreto and Leeham, using ChatGPT and Aristotle, have proved a negative answer, which was quantified by Tao and Alexeev (see the comments).

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

Search problems.science

Find a Problem, Result, source, or page