Catalan's conjecture and related Diophantine equations

Conjecture · pillais_conjecture

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$ .

Formal statement · Lean 4.lean

theorem 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 := by
  sorry

Proof. sorry

Nobody has tried yet.

Reference ↗ · Lean source ↗