Prove2Me

lean_workbook_plus_10747

Proved

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

Prove that (n−2)(n−1)n(n+1)(n+2)(n+3)+3≡3(mod10).(n-2)(n-1)n(n+1)(n+2)(n+3)+3\equiv 3 \pmod {10}. for ∀n∈N.\forall {n}\in\mathbb{N}.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_10747 : ∀ n : ℕ, ((n-2)*(n-1)*n*(n+1)*(n+2)*(n+3)+3) % 10 = 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph