lean_workbook_plus_9656

Proved

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

Consider the equation modulo 4. We have $x^{2}-2\equiv-y\pmod{4}$ . Since $x^2$ can be congruent to only 0 or 1 mod 4, $y$ is congruent to 1 or 2 mod 4.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9656 {x y : ℤ} (h : x^2 - 2 ≡ -y [ZMOD 4]) : y ≡ 1 [ZMOD 4] ∨ y ≡ 2 [ZMOD 4]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph