1. FormalConjectures
  2. ErdosProblems
  3. «364»
/- Copyright 2025 The Formal Conjectures Authors. Licensed under the Apache License, Version 2.0 (the "License"); you may not use this file except in compliance with the License. You may obtain a copy of the License at https://www.apache.org/licenses/LICENSE-2.0 Unless required by applicable law or agreed to in writing, software distributed under the License is distributed on an "AS IS" BASIS, WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied. See the License for the specific language governing permissions and limitations under the License. -/ import FormalConjecturesUtil

Erdős Problem 364

Reference: erdosproblems.com/364

open Nat namespace Erdos364

There is no consecutive triple of powerful numbers.

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_364 : ¬ ∃ (n : ℕ), Powerful n ∧ Powerful (n + 1) ∧ Powerful (n + 2) := ⊢ ¬∃ n, n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful All goals completed! 🐙

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.

@[category research open, AMS 11] theorem declaration uses 'sorry'erdos_364.variants.strong : ∃ (c : ℝ) (h : c > 0), ∀ (k : ℕ), Nat.nth Powerful (k + 2) - Nat.nth Powerful k > (Nat.nth Powerful k : ℝ) ^ c := ⊢ ∃ c, ∃ (_ : c > 0), ∀ (k : ℕ), ↑(nth Powerful (k + 2)) - ↑(nth Powerful k) > ↑(nth Powerful k) ^ c All goals completed! 🐙

There is no quadruple of powerful numbers, since at least one of the four numbers must be $2 \pmod{4}$, which cannot be powerful (since $2$ divides it, but $2^2$ does not).

@[category textbook, AMS 11] theorem erdos_364.variants.weak : ¬ ∃ (n : ℕ), Powerful n ∧ Powerful (n + 1) ∧ Powerful (n + 2) ∧ Powerful (n + 3) := ⊢ ¬∃ n, n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerful h:∃ n, n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerful⊢ False n:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerful⊢ False have h2mod4 : n % 4 = 2 ∨ (n + 1) % 4 = 2 ∨ (n + 2) % 4 = 2 ∨ (n + 3) % 4 = 2 := ⊢ ¬∃ n, n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerful All goals completed! 🐙 n:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerfulh✝:n % 4 = 2⊢ Falsen:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerfulh✝:(n + 1) % 4 = 2⊢ Falsen:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerfulh✝:(n + 2) % 4 = 2⊢ Falsen:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerfulh✝:(n + 3) % 4 = 2⊢ False n:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerfulh✝:n % 4 = 2⊢ Falsen:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerfulh✝:(n + 1) % 4 = 2⊢ Falsen:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerfulh✝:(n + 2) % 4 = 2⊢ Falsen:ℕhn:n.Powerful ∧ (n + 1).Powerful ∧ (n + 2).Powerful ∧ (n + 3).Powerfulh✝:(n + 3) % 4 = 2⊢ False All goals completed! 🐙 end Erdos364