Prove2Me

lean_workbook_plus_65893

Proved

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

n≡0(mod3)⇒3n(n+1)+7≡7(mod9)n\equiv 0\pmod{3}\Rightarrow 3n(n+1)+7\equiv 7\pmod{9}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65893 : ∀ n : ℤ, n % 3 = 0 → (3 * n * (n + 1) + 7) % 9 = 7 % 9   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph