lean_workbook_plus_33727

Proved

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

Find all triples of real numbers $(x, y, z)$ that satisfy the system of equations\n\n

\frac{1}{3} \min\{x,y\} + \frac{2}{3} \max\{x,y\} = 2017

\frac{1}{3} \min\{y,z\} + \frac{2}{3} \max\{y,z\} = 2018

\frac{1}{3} \min\{z,x\} + \frac{2}{3} \max\{z,x\} = 2019.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33727 (x y z : ℝ) : (x = 2018 ∧ y = 2015 ∧ z = 2019.5 ↔ 1/3 * min x y + 2/3 * max x y = 2017 ∧ 1/3 * min y z + 2/3 * max y z = 2018 ∧ 1/3 * min z x + 2/3 * max z x = 2019)   :=  by sorry

Source

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

View graph