Prove2Me

A four-variable weighted linear difference ratio sum is nonnegative

Proved
WorkbookSource.base_15586

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

lean-workbooksource-checked

a,b,c,d>0a,b,c,d>0 ,prove

3 d−a−b−c2 a2+2 b2+2 c2+d(a+b+c)+3 a−b−c−d2 b2+2 c2+2 d2+a(b+c+d)+3 b−c−d−a2 c2+2 d2+2 a2+b(a+c+d)+3 c−d−a−b2 d2+2 a2+2 b2+c(d+a+b)≥0{\frac {3\,d-a-b-c}{2\,{a}^{2}+2\,{b}^{2}+2\,{c}^{2}+d \left( a+b+c \right) }}+{\frac {3\,a-b-c-d}{2\,{b}^{2}+2\,{c}^{2}+2\,{d}^{2}+a \left( b+c+d \right) }}+{\frac {3\,b-c-d-a}{2\,{c}^{2}+2\,{d}^{2}+2\,{a}^{2}+b \left( a+c+d \right) }}+{\frac {3\,c-d-a-b}{2\,{d}^{2}+2\,{a}^{2}+2\,{b}^{2}+c \left( d+a+b \right) }}\geq 0

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_15586 (a b c d : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) : (3 * d - a - b - c) / (2 * a ^ 2 + 2 * b ^ 2 + 2 * c ^ 2 + d * (a + b + c)) + (3 * a - b - c - d) / (2 * b ^ 2 + 2 * c ^ 2 + 2 * d ^ 2 + a * (b + c + d)) + (3 * b - c - d - a) / (2 * c ^ 2 + 2 * d ^ 2 + 2 * a ^ 2 + b * (a + c + d)) + (3 * c - d - a - b) / (2 * d ^ 2 + 2 * a ^ 2 + 2 * b ^ 2 + c * (d + a + b)) ≥ 0  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_15586; Apache-2.0

View graph