lean_workbook_plus_3950

Proved

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

Another way is to observe that, for integers $n$ and $k$ , $(3n + k)^3 = 27n^3 + 27nk^2 + 9n^2k + k^3 \equiv k^3 \mod 9.$ Since any integer can be written as $3n + k$ for $k = 0$ , $1$ , or $2$ , it follows that its cube must be congruent to $0^3$ , $1^3$ , or $2^3$ mod $9$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_3950  (n k : ℤ)
  (h₀ : 0 ≤ k ∧ k ≤ 2) :
  (3 * n + k)^3 % 9 = k^3 % 9   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph