Lean-Workbook Syntax 55924: Seven consecutive cubes sum to a multiple of seven

Proved

WorkbookSyntax.plus_55924

by wamlart · Sep 12, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

lean-workbookrepaired-notationsource-checked

For every integer $a$ , $\sum_{i=0}^{6}(a+i)^3\equiv0\pmod7$ .

Source: Lean-Workbook row lean_workbook_plus_55924 (Apache-2.0), original record. This corrected declaration replaces the obsolete finite sum/product binder in with ∈ and restores required imports or namespaces. Ranges, casts, quantifiers, and mathematical expressions are preserved.

Preamble

import Mathlib.Data.Int.ModEq
import Mathlib.Algebra.BigOperators.Ring.Finset

Formal statement

theorem WorkbookSyntax.plus_55924 (a : ℤ) :
    ∑ i ∈ Finset.range 7, (a + i) ^ 3 ≡ 0 [ZMOD 7]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_55924; immutable original Prove2Me node b6aa43c0-59b3-4344-b30a-a2d83e6b7022

View graph