Prove2Me

A weighted mixed quadratic ratio sum is at least nine halves

Proved
WorkbookSource.base_35577

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

lean-workbooksource-checked

Let x,y,z>0x,y,z>0 ,prove that

2 x2+yzy2+z2+2 y2+xzx2+z2+2 z2+xyx2+y2≥92{\frac {2\,{x}^{2}+yz}{{y}^{2}+{z}^{2}}}+{\frac {2\,{y}^{2}+xz}{{x}^{2}+{z}^{2}}}+{\frac {2\,{z}^{2}+xy}{{x}^{2}+{y}^{2}}}\geq \frac{9}{2}

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

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

View graph