Prove2Me

lean_workbook_plus_20020

Proved

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

Find the maximum and minimum of A=x2+y2+z2+kxyzA=x^2+y^2+z^2+kxyz, where x,y,zx, y, z are non-negative numbers satisfying x+y+z=1x+y+z=1, for all k∈Rk \in R.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_20020 (x y z k : ℝ) (hx : 0 ≤ x) (hy : 0 ≤ y) (hz : 0 ≤ z) (hx1 : x + y + z = 1) : (x^2 + y^2 + z^2 + k * x * y * z) ≤ 1 + k/27 ∨ (x^2 + y^2 + z^2 + k * x * y * z) ≥ 1 + k/27   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph