Prove2Me

lean_workbook_plus_910

Proved

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

LHS-RHS=\n12((a−b)2(a+b−c)2+(b−c)2(b+c−a)2+(c−a)2(c+a−b)2)⩾0.\frac{1}{2}((a-b)^2(a+b-c)^2+(b-c)^2(b+c-a)^2+(c-a)^2(c+a-b)^2)\geqslant 0.

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

View graph