Skip to content

Erdős problem 369

Start work

Let ϵ>0\epsilon>0 and k≥2k\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?

No current result

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

Retained declaration

FormalConjectures/ErdosProblems/369.lean

Formal Conjectures

FormalConjectures/ErdosProblems/369.leanErdos369.erdos_3697 linesExact file
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 ^ ε
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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:369
  • PLBY Lean proofsErdosProblems.Erdos369

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry