Prove2Me

lean_workbook_plus_15802

Proved

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

Solution which induction: Suppose that 9n+1−8n−9⋮649^{n+1}-8n-9\vdots64 , we have 9n+2−8(n+1)−9=9(9n+1−8n−9)+72n+81−8n−8−9=9(9n+1−8n−9)+64n−64⋮649^{n+2}-8(n+1)-9=9(9^{n+1}-8n-9)+72n+81-8n-8-9=9(9^{n+1}-8n-9)+64n-64\vdots64

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_15802  (n : ℕ) :
  9^(n + 1) - 8 * n - 9 ≡ 0 [ZMOD 64]   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph