FormalConjectures.ErdosProblems.«939»

/-
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 939

Reference: erdosproblems.com/939

open Nat


namespace Erdos939

A set S belongs to Erdos939Sums r if it meets the following criteria:

The size of the set is $|S| = r - 2$ .

The elements of the set are coprime (their greatest common divisor is 1).

Every element in S is an $r$-powerful number.

The sum of the elements in S, i.e., $\sum_{s \in S} s$ , is also an $r$-powerful number.

def Erdos939Sums (r : ℕ) :=
    {S : Finset ℕ | S.card = r - 2 ∧ S.Coprime ∧ r.Full (∑ s ∈ S, s) ∧ ∀ s ∈ S, r.Full s}

If $r≥4$ then can the sum of $r-2$ coprime $r$-powerful numbers ever be itself $r$-powerful?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_939 : answer(sorry) ↔ ∀ r ≥ 4, (Erdos939Sums r).Nonempty := by⊢ True ↔ ∀ r ≥ 4, (Erdos939Sums r).Nonempty
  sorryAll goals completed! 🐙

If $r≥4$ are there infinitely many sums of $r-2$ coprime $r$-powerful numbers that are themselves $r$-powerful?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_939.variants.infinite : answer(sorry) ↔ ∀ r ≥ 4, (Erdos939Sums r).Infinite := by⊢ True ↔ ∀ r ≥ 4, (Erdos939Sums r).Infinite
  sorryAll goals completed! 🐙

Are there infinitely many triples of coprime $3$-powerful numbers $a, b, c$ such that $a + b = c$?

@[category research open, AMS 11]
theorem declaration uses 'sorry'erdos_939.variants.triples :
    answer(sorry) ↔ {(a,b,c) | ({a, b, c} : Finset ℕ).Coprime ∧
      (3).Full a ∧ (3).Full b ∧ (3).Full c ∧
      a + b = c}.Infinite := by⊢ True ↔ {(a, b, c) | {a, b, c}.Coprime ∧ Full 3 a ∧ Full 3 b ∧ Full 3 c ∧ a + b = c}.Infinite
  sorryAll goals completed! 🐙

Cambie has found several examples of the sum of $r - 2$ coprime $r$-powerful numbers being itself $r$-powerful. For example when $r=5$ we have $$3761^5=2^8\cdot3^{10}\cdot 5^7 + 2^{12}\cdot 23^6 + 11^5\cdot 13^5$$.

@[category research solved, AMS 11]
theorem erdos_939.variants.examples : (∃ r ≥ 4, (Erdos939Sums r).Nonempty) := by⊢ ∃ r ≥ 4, (Erdos939Sums r).Nonempty
  use 5h⊢ 5 ≥ 4 ∧ (Erdos939Sums 5).Nonempty
  simp only [ge_iff_le, reduceLeDiff, true_and]h⊢ (Erdos939Sums 5).Nonempty
  unfold Erdos939Sumsh⊢ {S | S.card = 5 - 2 ∧ S.Coprime ∧ Full 5 (∑ s ∈ S, s) ∧ ∀ s ∈ S, Full 5 s}.Nonempty
  simp [Set.Nonempty]h⊢ ∃ S, S.card = 3 ∧ S.Coprime ∧ Full 5 (∑ s ∈ S, s) ∧ ∀ s ∈ S, Full 5 s
  use {2^8 * 3^10 * 5^7, 2^12 * 23^6, 11^5 * 13^5}h⊢ {2 ^ 8 * 3 ^ 10 * 5 ^ 7, 2 ^ 12 * 23 ^ 6, 11 ^ 5 * 13 ^ 5}.card = 3 ∧
  {2 ^ 8 * 3 ^ 10 * 5 ^ 7, 2 ^ 12 * 23 ^ 6, 11 ^ 5 * 13 ^ 5}.Coprime ∧
    Full 5 (∑ s ∈ {2 ^ 8 * 3 ^ 10 * 5 ^ 7, 2 ^ 12 * 23 ^ 6, 11 ^ 5 * 13 ^ 5}, s) ∧
      ∀ s ∈ {2 ^ 8 * 3 ^ 10 * 5 ^ 7, 2 ^ 12 * 23 ^ 6, 11 ^ 5 * 13 ^ 5}, Full 5 s
  simph⊢ {1180980000000, 606355001344, 59797108943}.Coprime ∧
  Full 5 1847132110287 ∧ Full 5 1180980000000 ∧ Full 5 606355001344 ∧ Full 5 59797108943
  constructorh.left⊢ {1180980000000, 606355001344, 59797108943}.Coprimeh.right⊢ Full 5 1847132110287 ∧ Full 5 1180980000000 ∧ Full 5 606355001344 ∧ Full 5 59797108943
  ·h.left⊢ {1180980000000, 606355001344, 59797108943}.Coprime unfold Finset.Coprimeh.left⊢ {1180980000000, 606355001344, 59797108943}.gcd id = 1
    aesopAll goals completed! 🐙
  ·h.right⊢ Full 5 1847132110287 ∧ Full 5 1180980000000 ∧ Full 5 606355001344 ∧ Full 5 59797108943 norm_num [Nat.Full, Nat.primeFactors, Nat.primeFactorsList]All goals completed! 🐙

Cambie has also found solutions when $r=7$.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_939.variants.seven : (Erdos939Sums 7).Nonempty := by⊢ (Erdos939Sums 7).Nonempty
  sorryAll goals completed! 🐙

Cambie has also found solutions when $r=8$.

@[category research solved, AMS 11]
theorem declaration uses 'sorry'erdos_939.variants.eight : (Erdos939Sums 8).Nonempty := by⊢ (Erdos939Sums 8).Nonempty
  sorryAll goals completed! 🐙

Euler had conjectured that the sum of $k - 1$ many $k$-th powers is never a $k$-th power, but this is false for $k=5$, as Lander and Parkin [LaPa67] found $$27^5+84^5+110^5+133^5=144^5$$.

[LaPa67] Lander, L. J. and Parkin, T. R., "A counterexample to Euler's sum of powers conjecture." Math. Comp. (1967), 101--103.

@[category research solved, AMS 11]
theorem erdos_939.variants.euler : ¬ (∀ k ≥ 4, ∀ S : Finset ℕ, S.card = k - 1 →
    ¬ (∃ q, ∑ s ∈ S, s ^ k = q ^k)) := by⊢ ¬∀ k ≥ 4, ∀ (S : Finset ℕ), S.card = k - 1 → ¬∃ q, ∑ s ∈ S, s ^ k = q ^ k
  push_neg⊢ ∃ k ≥ 4, ∃ S, S.card = k - 1 ∧ ∃ q, ∑ s ∈ S, s ^ k = q ^ k
  use 5h⊢ 5 ≥ 4 ∧ ∃ S, S.card = 5 - 1 ∧ ∃ q, ∑ s ∈ S, s ^ 5 = q ^ 5
  norm_numh⊢ ∃ S, S.card = 4 ∧ ∃ q, ∑ s ∈ S, s ^ 5 = q ^ 5
  use {27, 84, 110, 133}h⊢ {27, 84, 110, 133}.card = 4 ∧ ∃ q, ∑ s ∈ {27, 84, 110, 133}, s ^ 5 = q ^ 5
  constructorh.left⊢ {27, 84, 110, 133}.card = 4h.right⊢ ∃ q, ∑ s ∈ {27, 84, 110, 133}, s ^ 5 = q ^ 5
  ·h.left⊢ {27, 84, 110, 133}.card = 4 decideAll goals completed! 🐙
  ·h.right⊢ ∃ q, ∑ s ∈ {27, 84, 110, 133}, s ^ 5 = q ^ 5 use 144h⊢ ∑ s ∈ {27, 84, 110, 133}, s ^ 5 = 144 ^ 5
    norm_numAll goals completed! 🐙


end Erdos939