lean_workbook_plus_32028

Proved

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

Let $x$ , $y$ , and $z$ be positive real numbers with $x+y+z = 3$ . Prove that at least one of the three numbers\n\n $x(x+y-z)$ \n $y(y+z-x)$ \n $z(z+x-y)$ \nis less or equal $1$ .\n\n(Karl Czakler)

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32028 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) (h : x + y + z = 3) : ∃ x y z : ℝ, (x + y + z = 3 ∧ (x * (x + y - z) ≤ 1 ∨ y * (y + z - x) ≤ 1 ∨ z * (z + x - y) ≤ 1))   :=  by sorry

Source

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

View graph