lean_workbook_plus_7004

Proved

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

By $x,y,z\ge 1$ , we have $\sqrt {3 - 2x}\le 1$ etc., thus $LHS \le xy+yz+zx\le x^2 + y^2 + z^2\le x^3 + y^3 + z^3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7004 : ∀ x y z : ℝ, x ≥ 1 ∧ y ≥ 1 ∧ z ≥ 1 → Real.sqrt (3 - 2 * x) ≤ 1 ∧ Real.sqrt (3 - 2 * y) ≤ 1 ∧ Real.sqrt (3 - 2 * z) ≤ 1 → x * y + y * z + z * x ≤ x ^ 2 + y ^ 2 + z ^ 2 ∧ x ^ 2 + y ^ 2 + z ^ 2 ≤ x ^ 3 + y ^ 3 + z ^ 3   :=  by sorry

Source

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

View graph