Number theory

Erdős 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

. [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.

References

erdosproblems.com/364

No one has attempted this yet.

Formal statement

Lean type

∃ c,
  ∃ (_ : c > 0), ∀ (k : ℕ), ↑(Nat.nth Nat.Powerful (k + 2)) - ↑(Nat.nth Nat.Powerful k) > ↑(Nat.nth Nat.Powerful k) ^ c

What you must prove

import FormalConjectures.ErdosProblems.«364»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos364.erdos_364.variants.strong" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/364.lean

Source type SHA-256: sha256:75d67372a1eaebb2b5514dc15a2b850d0e5b32a9ee11d982594225c63d31838c
Task id: fc-379fc029-variants-strong-bc498ab635-formalized-v1
Task commitment: sha256:96ff5e43714fe8674037ff114ff48813a4c7a4fc8d3b167302d42daf2c3a57ac

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.