Catalan's Conjecture (Mihailescu, 2002)

import Mathlib

-- The only solution to xᵃ = yᵇ + 1 with x,y,a,b > 1 is 3² = 2³ + 1.
theorem catalan_conjecture (x y a b : ℕ)
    (hx : 1 < x) (hy : 1 < y) (ha : 1 < a) (hb : 1 < b)
    (h : x ^ a = y ^ b + 1) :
    x = 3 ∧ a = 2 ∧ y = 2 ∧ b = 3 :=
    sorry