Skip to content

Erdős problem 369

Let ϵ>0\epsilon>0 and k2k\geq 2. Is it true that, for all sufficiently large nn, there is a sequence of kk consecutive integers in {1,,n}\{1,\ldots,n\} all of which are nϵn^\epsilon-smooth?

Sources

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

1 retained statement2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

369.lean

Retained formal statement1 of 1

Let ϵ>0\epsilon>0 and k2k\geq 2. Is it true that, for all sufficiently large nn, there is a sequence of kk consecutive integers in {1,,n}\{1,\ldots,n\} all of which are nϵn^\epsilon-smooth?

The problem is trivially true as written (simply taking {1,,k}\{1,\ldots,k\} and n>k1/ϵn>k^{1/\epsilon}). 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 mPm\in P (where PP is the sequence of kk consecutive integers sought for) must be in [n/2,n][n/2,n]. In this case a positive answer also follows directly from the result of Balog and Wooley [BaWo98] for infinitely many nn. Proving this is true for all large nn does not follow immediately from [BaWo98], but can be deduced using a similar construction, as shown by SkyYang.

FormalConjectures/ErdosProblems/369.leanErdos369.erdos_3697 linesExact file
True  ∀ (ε : ℝ),    0 < ε →      ∀ (k : ℕ),        2 ≤ k          ∀ᶠ (n : ℕ) in Filter.atTop,a, n / 2 ≤ a + 1 ∧ a + kn ∧ ∀ j < k, ∀ p ∈ (a + 1 + j).primeFactors, ↑p ≤ ↑n ^ ε
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.

Search problems.science

Find a Problem, Result, source, or page