Prove2Me

lean_workbook_plus_24192

Proved

by Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)

We have\n\n LHS−RHS=1a2+b2+c2∑(a−b)2(a+b−3c)2(a+c)(b+c)⩾0.\mathrm{LHS - RHS} = \frac{1}{a^2+b^2+c^2} \sum \frac{(a-b)^2(a+b-\sqrt 3 c)^2}{(a+c)(b+c)} \geqslant 0. From above, the inequality also true for all a, b, ca,\,b,\,c are real numbers such that ab+bc+ca>0.ab+bc+ca>0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_24192 (a b c : ℝ) (hab : a * b + b * c + c * a > 0) : (1 / (a ^ 2 + b ^ 2 + c ^ 2)) * ((a - b) ^ 2 * (a + b - Real.sqrt 3 * c) ^ 2 / (a + c) / (b + c) + (b - c) ^ 2 * (b + c - Real.sqrt 3 * a) ^ 2 / (b + a) / (c + a) + (c - a) ^ 2 * (c + a - Real.sqrt 3 * b) ^ 2 / (c + b) / (a + b)) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph