lean_workbook_plus_36732

Open

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

Let $n$ equal the amount of gillyweed in the first cauldron. Our equation is: $n+n+1+n+1...+n+6=3(n+6)+3$ Expanding the left side gives us: $n+n+1+n+2...+n+6=3n+21$ Our equation is now: $7n+21=3n+21$ This means that: $4n=0$ Therefore, the amount of gillyweed in the first cauldron is $n=\boxed{0}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36732  (n : ℕ)
  (h₀ : ∑ k in Finset.Icc 0 6, (n + k) = 3 * (n + 6) + 3) :
  n = 0   :=  by sorry

Source

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

View graph