lean_workbook_plus_66907
ProvedFactor into . Either or must be even, so for it to be divisible by 6, one of the terms must be divisible by 3. The only way or isn't divisible by 3 is if and . However, in this case, , so one of the three terms is always divisible by 3, and thus the expression is always divisible by 6.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_66907 : ∀ n : ℕ, 6 ∣ n * (n + 1) * (2 * n + 1) := by sorry
Source