lean_workbook_plus_65300

Proved

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

You can even try to prove that If $0 \leq x,y,z \leq 1$ then $2 \sum xy \leq 3xyz + \sum x$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65300 (x y z : ℝ) (hx : 0 ≤ x ∧ x ≤ 1) (hy : 0 ≤ y ∧ y ≤ 1) (hz : 0 ≤ z ∧ z ≤ 1) : 2 * (x*y + y*z + z*x) ≤ 3*x*y*z + x + y + z   :=  by sorry

Source

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

View graph