Euler's sum of powers conjecture

Euler's sum of powers conjecture says that at least n nth powers of positive integers are required to sum to an nth power of a positive integer.

This was an attempt to generalize Fermat's Last Theorem, which is the special case of summing 2 nth powers.

We demonstrate the connection with FLT, prove that it's true for n ≤ 3, and provide counterexamples for n = 4 and n = 5. The status of the conjecture for n ≥ 6 is unknown.

https://en.wikipedia.org/wiki/Euler%27s_sum_of_powers_conjecture http://euler.free.fr/

TODO

• Formalize Elkies's construction of infinitely many coprime counterexamples for n = 4 https://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/S0025-5718-1988-0930224-9.pdf

@[reducible, inline]

abbrev Counterexample.SumOfPowersConjectureWith (R : Type u_1) [Semiring R] (n : ℕ) : Prop

Euler's sum of powers conjecture over a given semiring with a specific exponent.

Equations

• Counterexample.SumOfPowersConjectureWith R n = ∀ (a : List R) (b : R), 2 ≤ a.length → 0 ∉ a → b ≠ 0 → (List.map (fun (x : R) => x ^ n) a).sum = b ^ n → n ≤ a.length

@[reducible, inline]

abbrev Counterexample.SumOfPowersConjectureFor (n : ℕ) : Prop

Euler's sum of powers conjecture over the naturals for a given exponent.

Equations

• Counterexample.SumOfPowersConjectureFor n = Counterexample.SumOfPowersConjectureWith ℕ n

@[reducible, inline]

abbrev Counterexample.SumOfPowersConjecture : Prop

Euler's sum of powers conjecture over the naturals.

Equations

• Counterexample.SumOfPowersConjecture = ∀ (n : ℕ), Counterexample.SumOfPowersConjectureFor n

theorem Counterexample.fermatLastTheoremWith_of_sumOfPowersConjectureWith (R : Type u_1) [Semiring R] (n : ℕ) : n ≥ 3 → SumOfPowersConjectureWith R n → FermatLastTheoremWith R n

Euler's sum of powers conjecture over a given semiring with a specific exponent implies FLT.

theorem Counterexample.fermatLastTheorem_of_sumOfPowersConjecture : SumOfPowersConjecture → FermatLastTheorem

Euler's sum of powers conjecture over the naturals implies FLT.

theorem Counterexample.sumOfPowersConjectureWith_three_iff_fermatLastTheoremWith_three (R : Type u_1) [Semiring R] : SumOfPowersConjectureWith R 3 ↔ FermatLastTheoremWith R 3

For n = 3, Euler's sum of powers conjecture over a given semiring is equivalent to FLT.

theorem Counterexample.sumOfPowersConjectureFor_le_three (n : ℕ) : n ≤ 3 → SumOfPowersConjectureFor n

Euler's sum of powers conjecture over the naturals is true for n ≤ 3.

theorem Counterexample.sumOfPowersConjecture_of_ringHom {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} (hf : ∀ (x : R), f x = 0 → x = 0) {n : ℕ} (conj : SumOfPowersConjectureWith S n) : SumOfPowersConjectureWith R n

Given a ring homomorphism from R to S with no nontrivial zeros, the conjecture over S implies the conjecture over R.

theorem Counterexample.sumOfPowersConjecture_of_injective {R : Type u_1} {S : Type u_2} [Semiring R] [Semiring S] {f : R →+* S} (hf : Function.Injective ⇑f) {n : ℕ} (h : SumOfPowersConjectureWith S n) : SumOfPowersConjectureWith R n

Given an injective ring homomorphism from R to S, the conjecture over S implies the conjecture over R.

theorem Counterexample.sumOfPowersConjectureFor_five_false : ¬SumOfPowersConjectureFor 5

The first counterexample was found by Leon J. Lander and Thomas R. Parkin in 1966 through a computer search, disproving the conjecture. https://www.ams.org/journals/bull/1966-72-06/S0002-9904-1966-11654-3/S0002-9904-1966-11654-3.pdf This is also the smallest counterexample for n = 5.

theorem Counterexample.sumOfPowersConjectureFor_four_false : ¬SumOfPowersConjectureFor 4

The first counterexample for n = 4 was found by Noam D. Elkies in October 1988: a := [2_682_440, 15_365_639, 18_796_760], b := 20_615_673 https://www.ams.org/journals/mcom/1988-51-184/S0025-5718-1988-0930224-9/S0025-5718-1988-0930224-9.pdf In this paper, Elkies constructs infinitely many solutions to a^4 + b^4 + c^4 = d^4 for coprime a, b, c, d, which provide infinitely many coprime counterexamples for the case n = 4. Here we use the smallest counterexample for n = 4, which was found a month later by Roger E. Frye https://ieeexplore.ieee.org/document/74138

@[reducible, inline]

abbrev Counterexample.ExistsEqualSumsOfLikePowersFor (R : Type u_1) [Semiring R] (k m n : ℕ) : Prop

For all (k, m, n) we define the Diophantine equation ∑ x_i ^ k = ∑ y_i ^ k where x and y are disjoint with length m and n respectively. This is a generalization of the diophantine equation of Euler's sum of powers conjecture.

Equations

• One or more equations did not get rendered due to their size.

theorem Counterexample.existsEqualSumsOfLikePowersFor_of_sumOfPowersConjectureWith (R : Type u_1) [Semiring R] (k m : ℕ) (hm : 2 ≤ m) : SumOfPowersConjectureWith R k → ExistsEqualSumsOfLikePowersFor R k m 1 → k ≤ m

Euler's sum of powers conjecture for k restricts solutions for (k, m, 1).

@[reducible, inline]

abbrev Counterexample.LanderParkinSelfridgeConjecture (R : Type u_1) [Semiring R] (k m n : ℕ) : Prop

After the first counterexample was found, Leon J. Lander, Thomas R. Parkin, and John Selfridge made a similar conjecture that is not amenable to the counterexamples found so far. The status of this conjecture is unknown. https://en.wikipedia.org/wiki/Lander,_Parkin,_and_Selfridge_conjecture https://www.ams.org/journals/mcom/1967-21-099/S0025-5718-1967-0222008-0/S0025-5718-1967-0222008-0.pdf

Equations

• Counterexample.LanderParkinSelfridgeConjecture R k m n = (Counterexample.ExistsEqualSumsOfLikePowersFor R k m n → k ≤ m + n)

theorem Counterexample.LanderParkinSelfridgeConjecture_of_sumOfPowersConjectureWith (R : Type u_1) [Semiring R] (k m : ℕ) (hm : 2 ≤ m) : SumOfPowersConjectureWith R k → LanderParkinSelfridgeConjecture R k m 1

Euler's sum of powers conjecture for k implies the Lander, Parkin, and Selfridge conjecture for (k, m, 1).