lean_workbook_plus_33307

Disproved

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

If $t=0\pmod{6}$ , then $1^t=2^t=4^t=5^t=7^t=8^t=1\pmod{9}$ , and the sum is $0\pmod{9}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33307  (t : ℕ)
  (h₀ : t % 6 = 0) :
  ((1^t + 2^t + 4^t + 5^t + 7^t + 8^t) % 9) = 0   :=  by sorry

Source