Erdős problem 369
Let and . Is it true that, for all sufficiently large , there is a sequence of consecutive integers in all of which are -smooth?
Sources
FormalConjectures/ErdosProblems/
369.lean
Let and . Is it true that, for all sufficiently large , there is a sequence of consecutive integers in all of which are -smooth?
The problem is trivially true as written (simply taking and ). There are (at least) two possible variants which are non-trivial, and it is not clear which Erdős and Graham meant. We formalize the second: each (where is the sequence of consecutive integers sought for) must be in . In this case a positive answer also follows directly from the result of Balog and Wooley [BaWo98] for infinitely many . Proving this is true for all large does not follow immediately from [BaWo98], but can be deduced using a similar construction, as shown by SkyYang.
True ↔ ∀ (ε : ℝ), 0 < ε → ∀ (k : ℕ), 2 ≤ k → ∀ᶠ (n : ℕ) in Filter.atTop, ∃ a, n / 2 ≤ a + 1 ∧ a + k ≤ n ∧ ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, ↑p ≤ ↑n ^ ε