Number theory · Last catalog review 26 Jul 2026

Erdős Problem 364

There is no consecutive triple of powerful numbers.

References

erdosproblems.com/364

Published 24 Jun 2026Never attempted

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-e923379e-erdos364-erdos-364-5b256fef06-formalized-v1
Task commitment: sha256:e2cd92312988224dd72627c56916615589edec6a3dd69850685b4cb7b5a481b2

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.