Erdős problem 205 · problems.science

Is it true that all sufficiently large $n$ can be written as $2^k+m$ for some $k\geq 0$ , where $\Omega(m)<\log\log m$ ? (Here $\Omega(m)$ is the number of prime divisors of $m$ 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 statement4 of 5

In fact there are infinitely many $n$ such that, for all $k$ with $2^k<n$ , $n-2^k$ has at least $\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

1∃ c > 0,2  {n |3      ∀ (k : ℕ),4        2 ^ k < n →5          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.

Sources

Search problems.science