Prove2Me

A cyclic quadratic ratio sum with a normalized product correction

Proved
WorkbookSource.plus_39495

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

lean-workbooksource-checked

For a,b,c>0a, b, c>0 prove that a2+b2−a(b−c)(b+c)(c+a)+b2+c2−b(c−a)(c+a)(a+b)+c2+a2−c(a−b)(a+b)(b+c)+2abc(a+b)(b+c)(c+a)≥74\frac{a^2+b^2-a(b-c)}{(b+c)(c+a)}+\frac{b^2+c^2-b(c-a)}{(c+a)(a+b)}+\frac{c^2+a^2-c(a-b)}{(a+b)(b+c)}+\frac{2abc}{(a+b)(b+c)(c+a)}\ge\frac{7}{4}

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

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

View graph