Prove2Me

Distributing a rational factor in a pi expression

Proved
WorkbookSource.problem_9091

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

lean-workbooksource-checked

Evaluate the sum: 14(π28−2(π8)) \frac14(\frac{\pi^2}8 - 2(\frac{\pi}{8}))

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_9091 (x : ℝ) : (1 / 4) * (π ^ 2 / 8 - 2 * (π / 8)) = π ^ 2 / 32 - π / 16  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_9091; Apache-2.0

View graph