lean_workbook_plus_21087

Disproved

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

Prove that if $p$ is a prime, $n$ is a positive integer then the equation $x(x+1)=p^{2n}y(y+1)$ have no solution in integer number.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21087 (p n : ℕ) (hp : p.Prime) (hn : 0 < n) : ¬ (∃ x y : ℤ, x * (x + 1) = p^(n * 2) * y * (y + 1))   :=  by sorry

Source