Consecutive smooth numbers

DefinitionErdős Problem 369, location variant#✓fully proved

This is the statement that for every real \(\varepsilon > 0\) and every natural number \(k \ge 2\) there is a natural number \(N\) such that for every natural number \(n \ge N\) there is a natural number \(a\) with \(\lfloor n/2 \rfloor \le a + 1\) and \(a + k \le n\) for which every prime factor \(p\) of each of the \(k\) consecutive integers \(a + 1, \dots, a + k\) satisfies \(p \le n^\varepsilon\).

Erdős Problem 369 as written allows the run anywhere in \(\{1, \dots, n\}\), which is trivially true (take \(1, \dots, k\) once \(n^\varepsilon \ge k\)); here the run must start at or after \(\lfloor n/2 \rfloor\).

def conjecture : Prop :=
  ∀ ε : Real, 0 < ε →
    ∀ k : Nat, 2 ≤ k →
      ∃ N : Nat, ∀ n : Nat, N ≤ n →
        ∃ a : Nat, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧
          ∀ j : Nat, j < k →
            ∀ p ∈ (a + 1 + j).primeFactors, (p : Real) ≤ (n : Real) ^ ε

Used by 1

Used bySolution of Erdős Problem 369, location variant

TheoremSolution of Erdős Problem 369, location variant#●ready to prove

For every real \(\varepsilon > 0\) and every natural number \(k \ge 2\) there is a natural number \(N\) such that for every natural number \(n \ge N\) there is a natural number \(a\) with \(\lfloor n/2 \rfloor \le a + 1\) and \(a + k \le n\) for which every prime factor \(p\) of each of the \(k\) consecutive integers \(a + 1, \dots, a + k\) satisfies \(p \le n^\varepsilon\).

public theorem_wanted conjecture_holds : conjecture

Sources

• Balog-Wooley 1998; Bober-Fretwell-Martin-Wooley 2020.
• Lean proof of EP-369 location variant (plby/lean-proofs), https://github.com/plby/lean-proofs/blob/1d7b3f00780b85ed0462e79a1cd5650ee9055655/src/v4.29.1/ErdosProblems/Erdos369.lean.

Uses 1

Statement usesErdős Problem 369, location variant

1 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.