lean_workbook_plus_29437

Proved

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

Real Solution $30 \cdot \frac{1}{2} \cdot \frac{2}{3} \cdot \frac{4}{5} = \boxed{8}.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_29437 (a b c d : ℝ) (h₁ : a = 30) (h₂ : b = 1 / 2) (h₃ : c = 2 / 3) (h₄ : d = 4 / 5) : a * b * c * d = 8   :=  by sorry

Source