lean_workbook_plus_72010Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)Find all triples of reals (x,y,z)(x,y,z)(x,y,z) satisfying: \n\n {13min{x,y}+23max{x,y}=2017 13min{y,z}+23max{y,z}=2018 13min{z,x}+23max{z,x}=2019\begin{cases} \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 \end{cases}{31min{x,y}+32max{x,y}=2017 31min{y,z}+32max{y,z}=2018 31min{z,x}+32max{z,x}=2019Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_72010 (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 sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph