lean_workbook_plus_13960

Proved

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

If $x$ is the average (arithmetic mean) of $m$ and $9$ , $y$ is the average of $2m$ and $15$ , and $z$ is the average of $3m$ and $18$ , what is the average of $x$ , $y$ , and $z$ in terms of $m$ ?

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_13960 (m x y z : ℝ) (hx : x = (m + 9) / 2) (hy : y = (2 * m + 15) / 2) (hz : z = (3 * m + 18) / 2) : (x + y + z) / 3 = m + 7   :=  by sorry

Source

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

View graph