Prove2Me

lean_workbook_plus_21450

Proved

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

Using the well-known inequality x+y+z≥3(xy+xz+yz)x+y+z\ge \sqrt{3(xy+xz+yz)} and the given condition xy+xz+yz≥3xy+xz+yz\ge 3, prove that x2+y2+z2+xy+xz+yz+3(x+y+z)2≤x2+y2+z2+2(xy+xz+yz)(x+y+z)2=1\frac{x^2+y^2+z^2+xy+xz+yz+3}{(x+y+z)^2} \le \frac{x^2+y^2+z^2+2(xy+xz+yz)}{(x+y+z)^2}=1.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_21450 (x y z : ℝ) (h : x * y + x * z + y * z ≥ 3) : (x ^ 2 + y ^ 2 + z ^ 2 + x * y + x * z + y * z + 3) / (x + y + z) ^ 2 ≤ 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph