Skip to content

Erdős problem 1139

Let 1≤u1<u2<⋯1\leq u_1 < u_2 < \cdots be the sequence of integers with at most 22 prime factors. Is it true that lim sup⁡k→∞uk+1−uklog⁡k=∞?\limsup_{k \to \infty} \frac{u_{k+1}-u_k}{\log k}=\infty?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/1139.lean

Formal Conjectures

FormalConjectures/ErdosProblems/1139.leanErdos1139.erdos_11398 linesExact file
True ↔  Filter.limsup      (fun k =>        (↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) (k + 1)) -            ↑↑(Nat.nth (fun n => 0 < n ∧ ArithmeticFunction.cardFactors n ≤ 2) k)) /          ↑(Real.log (↑k + 1)))      Filter.atTop =    ⊤
OpenStatement only, no proof

Reported activity

Work these sources record against this Problem. Source-reported attribution, not reviewed here.

  • AI collaborating with humans

    Erdős AI contributions wiki · 26 Jan-19 Jun, 2026

    Machine
    GPT-5.2 Pro, GPT-5.5 Pro
    People
    Przemek Chojecki, gavinsherry, Liam Price, Terence Tao
    Open the source record

Continue

Start a contributionBrowse the source filesOpen the collection entry

Search problems.science

Find a Problem, Result, source, or page