Prove2Me

A cyclic quadratic difference ratio sum is nonnegative

Proved
WorkbookSource.base_51967

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

lean-workbooksource-checked

Prove the inequality for x,y,z>0x, y, z > 0: 0≤(x−y)(x−2y)(x+2z)(z+x)+(y−z)(y−2z)(x+y)(y+2x)+(z−x)(z−2x)(y+z)(z+2y)0 \leq \frac{(x - y)(x - 2y)}{(x + 2z)(z + x)} + \frac{(y - z)(y - 2z)}{(x + y)(y + 2x)} + \frac{(z - x)(z - 2x)}{(y + z)(z + 2y)}

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

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

View graph