lean_workbook_plus_54229

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

Now write the given relation as : $(2x+1)^2=(p^n(2y+1))^2-p^{2n}+1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_54229 (p : ℕ) (hp : p.Prime) (n : ℕ) (h : p > 2) : ∃ x y : ℕ, (2*x+1)^2 = (p^n * (2*y+1))^2 - p^(2*n) + 1   :=  by sorry

Source