Zero_and_One_are_the_only_Consecutive_Perfect_Squares

Proved

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

proofwikisquare-numberszero-and-one-are-the-only-consecutive-perfect-squares

If $n$ is a perfect square other than $0$ , then $n+1$ is not a perfect square.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem Zero_and_One_are_the_only_Consecutive_Perfect_Squares (m : ℕ) (hm : m > 0) (k : ℕ) (hk : m ^ 2 + 1 = k ^ 2) : False := by sorry

Source