The first two terms of a rational geometric series

Proved

WorkbookSource.problem_8681

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Calculate the sum of the first two terms of the geometric series with $a = 2$ and $r = \frac{1}{3}$

Source: InternLM Lean-Workbook, record lean_workbook_8681 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_8681 (a r n : ℝ) (ha : a = 2) (hr : r = 1/3) (hn : n = 2) : a + a*r = 8/3  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_8681; Apache-2.0

View graph