Erdős problem 1139 · problems.science

Let $1\leq u_1 < u_2 < \cdots$ be the sequence of integers with at most $2$ prime factors. Is it true that $\limsup_{k \to \infty} \frac{u_{k+1}-u_k}{\log k}=\infty?$

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

1139.lean

Retained formal statement1 of 1

Let $1\leq u_1 < u_2 < \cdots$ be the sequence of integers with at most $2$ prime factors. Is it true that $\limsup_{k \to \infty} \frac{u_{k+1}-u_k}{\log k}=\infty?$

FormalConjectures/ErdosProblems/1139.leanErdos1139.erdos_11398 linesExact file

1True ↔2  Filter.limsup3      (fun k =>4        (↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) (k + 1)) -5            ↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) k)) /6          ↑(Real.log (↑k + 1)))7      Filter.atTop =8    ⊤

OpenStatement only, no proof

Sources

Search problems.science