Skip to content

Erdős problem 205

Start work

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

The source's own material, retained exactly.

5 retained statements36c6d0fef71a

Open selected source

FormalConjectures/ErdosProblems/

205.lean

Retained formal statement4 of 5

In fact there are infinitely many nn such that, for all kk with 2k<n2^k<n, n−2kn-2^k has at least ≫(log⁡nlog⁡log⁡n)1/2\gg \left(\frac{\log n}{\log\log n}\right)^{1/2} many prime factors.

FormalConjectures/ErdosProblems/205.leanErdos205.erdos_205.variants.many_prime_factors5 linesExact file
∃ c > 0,  {n |      ∀ (k : ℕ),        2 ^ k < n →          c * √(Real.log ↑n / Real.log (Real.log ↑n)) ≤ ↑(ArithmeticFunction.cardFactors (n - 2 ^ k))}.Infinite
SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.