Squares can hide distinct residues modulo three

Proved

WorkbookSource.problem_13238

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

In 6.2, when considering the congruence modulo 3, show that $x^2 \equiv y^2 \pmod{3}$ does not imply $x \equiv y \pmod{3}$ .

Source: InternLM Lean-Workbook, record lean_workbook_13238 (Apache-2.0). The complete source proposition and its explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_13238 : ∃ x y : ℤ, (x^2 ≡ y^2 [ZMOD 3]) ∧ ¬ (x ≡ y [ZMOD 3])  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_13238; Apache-2.0

View graph