Catalan's conjecture and related Diophantine equations

References:

• Wikipedia - Catalan's conjecture
• arXiv:2507.12397 (Lebesgue-Nagell equation)

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 < x ∧ 1 < y ∧ 1 < m ∧ 1 < n ∧ (m, n) ≠ (2, 2) ∧ a * x ^ n - b * y ^ m = c}.Finite

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

Lebesgue-Nagell equation

theorem LebesgueNagell.lebesgue_nagell (p : ℕ) (hp : Nat.Prime p) (hodd : Odd p) (x y : ℤ) : x ^ 2 - 2 = y ^ p ↔ (x = 1 ∨ x = -1) ∧ y = -1

Lebesgue-Nagell Equation Conjecture

For any odd prime $p$, the only integer solutions $(x, y)$ to the equation $x^2 - 2 = y^p$ are $(x, y) = (\pm 1, -1)$.

Reference: Ethan Katz and Kyle Pratt, "On the Lebesgue-Nagell equation $x^2 - 2 = y^p$", arXiv:2507.12397

theorem LebesgueNagell.lebesgue_nagell_solution_pos_one (p : ℕ) (hodd : Odd p) : 1 ^ 2 - 2 = (-1) ^ p

The pair $(1, -1)$ is a solution to $x^2 - 2 = y^p$ for any odd $p$.

theorem LebesgueNagell.lebesgue_nagell_solution_neg_one (p : ℕ) (hodd : Odd p) : (-1) ^ 2 - 2 = (-1) ^ p

The pair $(-1, -1)$ is a solution to $x^2 - 2 = y^p$ for any odd $p$.