Catalan's conjecture

Reference: Wikipedia

theorem Catalan.catalans_conjecture (a b x y : ℕ) (ha : 1 < a) (hb : 1 < b) (hx : 0 < x) (hy : 0 < y) (heq : x ^ a - y ^ b = 1) : a = 2 ∧ b = 3 ∧ x = 3 ∧ y = 2

The only natural number solution to the equation $x^a - y^b = 1$ such that $a, b > 1$ and $x, y > 0$ is given by $a = 2$, $b = 3$, $x = 3$, and $y = 2$.

theorem Catalan.pillais_conjecture (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : {(x, y, m, n) : ℕ × ℕ × ℕ × ℕ | 1 < m ∧ 1 < n ∧ a * x ^ n - b * y ^ m = c}.Finite

For positive integers a, b, and c, there are only finitely many solutions (x, y, m, n) to the equation $ax^n - by^m = c$ when $m, n > 1$.