Higher-degree Diophantine equations

Thue equations, generalized Fermat equations, sums of cubes, x^y = y^x, abc conjecture, Brocard–Ramanujan and symmetric-function equations.

TheoremExistence of seeds for generalized taxicab numbers#✓fully proved

Fix natural numbers \(m \ge 1\) and \(t \ge 1\), and let \(T(n, m, t)\) be, for each natural number \(n\), either a natural number or undefined, such that for all natural numbers \(n\) and \(v\), \(T(n, m, t)\) is defined and equals \(v\) exactly when \(v\) is the least natural number with at least \(t\) representations as a sum of exactly \(n\) positive \(m\)-th powers, representations being counted as unordered multisets of summands. Then there is a positive integer \(s_0\) such that \(T(s_0, m, t)\) is defined, say equal to \(v_0\), and \(T(s_0 + k, m, t) = v_0 + k\) for every natural number \(k\); moreover, \(s_0\) is the least positive integer \(s\) for which \(T(s, m, t)\) is defined and \(T(s + k, m, t) = T(s, m, t) + k\) for every natural number \(k\).

theorem generalized_taxicab_seed_exists
    (m t : ℕ) (hm : 1 ≤ m) (ht : 1 ≤ t)
    (T : ℕ → ℕ → ℕ → Option ℕ)
    (hT : ∀ n v : ℕ, T n m t = some v ↔
      (t ≤ Set.ncard {M : Multiset ℕ |
          M.card = n ∧ (∀ x ∈ M, 0 < x) ∧ (M.map (fun x => x ^ m)).sum = v} ∧
        ∀ v' : ℕ, v' < v →
          ¬ (t ≤ Set.ncard {M : Multiset ℕ |
            M.card = n ∧ (∀ x ∈ M, 0 < x) ∧ (M.map (fun x => x ^ m)).sum = v'}))) :
    ∃ s₀ : ℕ, 0 < s₀ ∧
      (∃ v₀ : ℕ, T s₀ m t = some v₀ ∧ ∀ k : ℕ, T (s₀ + k) m t = some (v₀ + k)) ∧
      ∀ s : ℕ, 0 < s →
        (∃ v : ℕ, T s m t = some v ∧ ∀ k : ℕ, T (s + k) m t = some (v + k)) →
        s₀ ≤ s
Sources

TheoremRational solutions of \(x^y = y^x\)#✓fully proved

If \(x\) and \(y\) are positive rational numbers with \(y < x\) and \(x^y = y^x\) (as real powers), then there is a positive integer \(v\) such that \(x = (1 + 1/v)^{v+1}\) and \(y = (1 + 1/v)^{v}\).

The source states \(v \in \mathbb{N}\); the reciprocal \(1/v\) forces \(v \ge 1\).

theorem rational_parametrization_pow_swap
    (x y : ℚ) (hx : 0 < x) (hy : 0 < y) (hyx : y < x)
    (h : (x : ℝ) ^ (y : ℝ) = (y : ℝ) ^ (x : ℝ)) :
    ∃ v : ℕ, 0 < v ∧
      x = (1 + 1 / (v : ℚ)) ^ (v + 1) ∧ y = (1 + 1 / (v : ℚ)) ^ v
Sources
  • Hirotaka Kobayashi, Kota Saito, and Wataru Takeda, "Transcendence of Values of the Iterated Exponential Function at Algebraic Points," Journal of Integer Sequences 26 (2023), Article 23.3.3, Lemma, lines 579–589, https://cs.uwaterloo.ca/journals/JIS/VOL26/Takeda/tak6.tex quoting Hurwitz.

TheoremSophie Germain's theorem#✓fully proved

Let \(p\) be an odd prime such that \(2p + 1\) is also prime. If \(x\), \(y\), \(z\) are pairwise coprime positive integers with \(x^p + y^p = z^p\), then \(p\) divides \(xyz\).

theorem sophieGermain (p x y z : ℕ) :
    Odd p → Nat.Prime p → Nat.Prime (2 * p + 1) →
    0 < x → 0 < y → 0 < z →
    Nat.Coprime x y → Nat.Coprime y z → Nat.Coprime x z →
    x ^ p + y ^ p = z ^ p → p ∣ x * y * z
Sources
  • https://en.wikipedia.org/wiki/Sophie_Germain%27s_theorem.

TheoremThe abc conjecture#●ready to prove

For every real \(\varepsilon > 0\) there is a real \(C_\varepsilon > 0\) such that for all integers \(a\), \(b\), \(c\) with \(a + b = c\) and \(\gcd(a, b) = 1\),

\[\max(|a|, |b|, |c|) \le C_\varepsilon \operatorname{rad}(abc)^{1 + \varepsilon},\]

where \(\operatorname{rad}(m)\) is the product of the distinct primes dividing \(|m|\), with \(\operatorname{rad}(0) = 1\).

public theorem_wanted abc_conjecture :
    ∀ ε : ℝ, 0 < ε → ∃ C : ℝ, 0 < C ∧ ∀ a b c : ℤ, a + b = c → Int.gcd a b = 1 →
      ((max (max a.natAbs b.natAbs) c.natAbs : ℕ) : ℝ) ≤
        C * ((∏ p ∈ (a * b * c).natAbs.primeFactors, (p : ℝ)) ^ (1 + ε))
Sources
  • Tsz Ho Chan, "Arithmetic Progressions Among Powerful Numbers", Journal of Integer Sequences 26 (2023), Article 23.1.1, Conjecture abc at source lines 111–117, https://cs.uwaterloo.ca/journals/JIS/VOL26/Chan/chan33.tex
3 fully proved1 ready to prove

The dependency explorer needs JavaScript and its graph data.

Download the complete graph data.