Source labels openChecked July 26, 2026

Erdős Problem 208: I

Let $s_1 < s_2 < \dots$ be the sequence of squarefree numbers. Is it true that for any $\epsilon > 0$ and large $n$ , $s_{n+1} - s_n \ll_\epsilon s_n^\epsilon$ ?

Number theory AMS 11

Mathematical statement

Let $s_1 < s_2 < \dots$ be the sequence of squarefree numbers. Is it true that for any $\epsilon > 0$ and large $n$ , $s_{n+1} - s_n \ll_\epsilon s_n^\epsilon$ ?

Statement source: Erdős Problems statement material

Statement terms: Source-specific

Source-specific terms. Therefore does not assert reuse rights beyond attributed display.

Statement artifacts, not proofs

These records expose exact Lean propositions and statement-only wrappers. Defining a proposition does not supply a proof of it. A placeholder-bearing target also contains no proof. Elaboration checks syntax and types; it does not certify that a formalization perfectly captures every nuance of the informal problem.

Pinned Lean formulation 1

erdos_208.parts.i

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_208.parts.i : answer(sorry) ↔    ∀ ε > (0 : ℝ), (fun n => (s (n + 1) - s n : ℝ)) =O[atTop] (fun n => (s n : ℝ)^ε) := by sorry /--Let $s_1 < s_2 < \dots$ be the sequence of squarefree numbers. Is it true that$s_{n + 1} - s_n \le (1 + o(1)) \cdot (\pi^2 / 6) \cdot \log (s_n) / \log (\log (s_n))$?-/@[category research open, AMS 11]theorem erdos_208.parts.ii : answer(sorry) ↔ ∃ (c : ℕ → ℝ), (c =o[atTop] (1 : ℕ → ℝ)) ∧ ∀ᶠ n in atTop,      s (n + 1) - s n ≤ (1 + (c n)) * (π^2 / 6) * log (s n) / log (log (s n)) := by  sorry

Statement source: Formal Conjectures
Lean version: v4.27.0
Placeholder: Present; no proof artifact
Source evidence: Pinned source index
Fidelity review: Community formulation

References

Pinned Formal Conjectures sourceformalization erdosproblems.com/208background