Number theory

Erdős 364

There is no consecutive triple of powerful numbers.

References

erdosproblems.com/364

No one has attempted this yet.

Formal statement

Lean type

¬∃ n, n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful

What you must prove

import FormalConjectures.ErdosProblems.«364»
import TaskSupport

namespace Bounty

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

end Bounty

Pinned source: FormalConjectures/ErdosProblems/364.lean

Source type SHA-256: sha256:51e0ea343d44a30c7155c0e6c37e1622325acb513949e3b88ea4bc5183337ff3
Task id: fc-379fc029-erdos364-erdos-364-d183dbf5d9-formalized-v1
Task commitment: sha256:85656e39e692519d5c0b69baf5e29c87dae6351897b09ca207dea80e301757f3

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.