Fermat-Catalan conjecture

Reference: Wikipedia

def FermatCatalanSet' : Set (Fin 6 → ℕ)

The set of solutions to the Fermat-Catalan Conjecture, i.e. the set of solutions $(a,b,c,m,n,k)$ to the equation $a^m + b^n = c^k$ where $\frac 1 m + \frac 1 n + \frac 1 k < 1$.

Equations

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

def FermatCatalanSet : Set (ℕ × ℕ × ℕ)

Equations

• FermatCatalanSet = (fun (f : Fin 6 → ℕ) => (f 0 ^ f 3, f 1 ^ f 4, f 2 ^ f 5)) '' FermatCatalanSet'

def FermatCatalanConjecture : Prop

The proposition that the Fermat-Catalan Conjecture is true.

Equations

• FermatCatalanConjecture = FermatCatalanSet.Finite

theorem fermat_catalan : FermatCatalanConjecture

The Fermat–Catalan conjecture states that the equation $a^m + b^n = c^k$ has only finitely many solutions $(a,b,c,m,n,k)$ with distinct triplets of values $(a^m, b^n, c^k)$ where $a, b, c$ are positive coprime integers and $m, n, k$ are positive integers satisfying $\frac 1 m + \frac 1 n + \frac 1 k < 1$.

theorem fermat_catalan.variants.darmon_granville (m n k : ℕ) (hm : 0 < m) (hn : 0 < n) (hk : 0 < k) (H : 1 / ↑m + 1 / ↑n + 1 / ↑k < 1) : {(a, b, c) : ℕ × ℕ × ℕ | 0 < a ∧ 0 < b ∧ 0 < c ∧ a ^ m + b ^ n = c ^ k ∧ {a, b, c}.Pairwise Nat.Coprime}.Finite

By the Darmon-Granville theorem, for any fixed choice of positive integers m, n and k satisfying $\frac 1 m + \frac 1 n + \frac 1 k < 1$, only finitely many coprime triples $(a, b, c)$ solving $a^m + b^n = c^k$ exist.