Prove2Me

A product of three quadratic factors with a triple-product correction

Proved
WorkbookSource.base_19226

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

For the minimum:

(x2+1)(y2+1)(z2+1)+4xyz(x+y+z)=[(1−xy)2+(x+y)2](z2+1)+4xyz(x+y+z)≥[z(1−xy)+(x+y)]2+4xyz(x+y+z)=(x+y+z−xyz)2+4xyz(x+y+z)=(x+y+z+xyz)2≥0\left(x^{2}+1\right)\left(y^{2}+1\right)\left(z^{2}+1\right)+4xyz(x+y+z) =\left[(1-xy)^{2}+(x+y)^{2}\right]\left(z^{2}+1\right)+4xyz(x+y+z) \ge\left[z(1-xy)+(x+y)\right]^{2}+4xyz(x+y+z) =(x+y+z-xyz)^{2}+4xyz(x+y+z) =(x+y+z+xyz)^{2} \ge0

Source: InternLM Lean-Workbook, record lean_workbook_19226 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_19226  (x y z : ℝ) :
  (x^2 + 1) * (y^2 + 1) * (z^2 + 1) + 4 * x * y * z * (x + y + z) ≥ 0  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_19226; Apache-2.0

View graph