Prove2Me

lean_workbook_plus_62333

Proved

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

p2−3p−2≡(p−10)2(mod17)p^2-3p-2 \equiv (p-10)^2 \pmod{17}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_62333 (p : ℕ) : p^2 - 3 * p - 2 ≡ (p - 10)^2 [ZMOD 17]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph