lean_workbook_plus_24238

Proved

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

Simplify: $\frac{1}{2} \times \frac{4}{5} \times \frac{10}{11} \times \frac{22}{23}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_24238 (a b c d : ℚ) (h₁ : a = 1 / 2) (h₂ : b = 4 / 5) (h₃ : c = 10 / 11) (h₄ : d = 22 / 23) : a * b * c * d = 8 / 23   :=  by sorry

Source

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

View graph