lean_workbook_plus_1784

Proved

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

Solution without Geometric Formula\n

\frac{7}{1} + \frac{7}{2} + \frac{7}{4} + \frac{7}{8}\cdots= x

We divide everything by 2: \n

\frac{7}{2} + \frac{7}{4} + \frac{7}{8} + \frac{7}{16}\cdots= \frac{x}{2}

We substitute the original equation in: \n

x-7=\frac{x}{2}

\frac{x}{2}=7

Therefore, $\boxed{x=14}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1784  (x : ℝ)
  (h₀ : ∑' k : ℕ, (7 / (2^k)) = x) :
  x = 14   :=  by sorry

Source