Source labels openChecked July 26, 2026

Erdős Problem 364: Strong

Erdős [Er76d] conjectured a stronger statement: if $n_k$ is the $k$ th powerful number, then $n_{k+2} - n_k > n_k^c$ for some constant $c > 0$ .

Number theory AMS 11

Mathematical statement

Erdős [Er76d] conjectured a stronger statement: if $n_k$ is the $k$ th powerful number, then $n_{k+2} - n_k > n_k^c$ for some constant $c > 0$ .

[Er76d] Erdős, P., Problems and results on number theoretic properties of consecutive integers and related questions. Proceedings of the Fifth Manitoba Conference on Numerical Mathematics (Univ. Manitoba, Winnipeg, Man., 1975) (1976), 25-44.

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_364.variants.strong

Canonical source

Complete statement target, proof intentionally absentLean 4

theorem erdos_364.variants.strong :    ∃ (c : ℝ) (h : c > 0), ∀ (k : ℕ),    Nat.nth Powerful (k + 2) - Nat.nth Powerful k > (Nat.nth Powerful k : ℝ) ^ c := 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/364background