Prove2Me

Evaluating a ratio of three products

Proved
WorkbookSource.problem_28817

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

lean-workbooksource-checked

Calculate 20×22×2410×11×12\frac{20\times 22\times 24}{10\times 11 \times 12} .

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.problem_28817 (a : ℚ) (h : a = 20 * 22 * 24 / (10 * 11 * 12)) : a = 8  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_28817; Apache-2.0

View graph