Prove2Me

A squared triangle-difference ratio sum with a quadratic correction

Proved
WorkbookSource.plus_73065

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

lean-workbooksource-checked

For a,b,c>0a, b, c>0 prove that (a+b−c)2(a+b)2+c2+(b+c−a)2(b+c)2+a2+(c+a−b)2(c+a)2+b2+1225⋅ab+bc+caa2+b2+c2≥2725\frac{(a+b-c)^2}{(a+b)^2+c^2}+\frac{(b+c-a)^2}{(b+c)^2+a^2}+\frac{(c+a-b)^2}{(c+a)^2+b^2}+\frac{12}{25}\cdot\frac{ab+bc+ca}{a^2+b^2+c^2} \ge \frac{27}{25}

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

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

View graph