Prove2Me

lean_workbook_plus_58227

Proved

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

An even square is congruent to 0(mod4),0 \pmod{4}, while an odd square is congruent to 1(mod4).1 \pmod{4}. This can be proven (2k)2=4k2=0(mod4)(2k)^2=4k^2=0 \pmod{4} ; (2k+1)2=4k2+4k+1=1(mod4)(2k+1)^2=4k^2+4k+1=1 \pmod{4} by representing even numbers as 2k2k and odd numbers as 2k+1.2k+1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_58227 : ∀ n : ℤ, Even n → n^2 % 4 = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph