Prove2Me

Lean-Workbook Syntax 36732: Solving a finite arithmetic-sum equation

Proved
WorkbookSyntax.plus_36732

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

lean-workbookrepaired-notationsource-checked

If a natural number nn satisfies ∑k=06(n+k)=3(n+6)+3\sum_{k=0}^{6}(n+k)=3(n+6)+3, then n=0n=0.

Source: Lean-Workbook row lean_workbook_plus_36732 (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.Algebra.BigOperators.Intervals
Formal statement
theorem WorkbookSyntax.plus_36732  (n : ℕ)
  (h₀ : ∑ k ∈ Finset.Icc 0 6, (n + k) = 3 * (n + 6) + 3) :
  n = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, row lean_workbook_plus_36732; immutable original Prove2Me node 7a434360-68ff-4776-8a32-fc0429424aa0

View graph