Catalan's conjecture and related Diophantine equations

Exercise · lebesgue_nagell_solution_pos_one

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

Formal statement · Lean 4.lean

theorem lebesgue_nagell_solution_pos_one (p : ℕ) (hodd : Odd p) :
    (1 : ℤ) ^ 2 - 2 = (-1 : ℤ) ^ p := by
  sorry

Proof. sorry

Nobody has tried yet.