Prove2Me

lean_workbook_plus_11860

Proved

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

Prove that (b2+c2−a2)(b−c)2+(c2+a2−b2)(c−a)2+(a2+b2−c2)(a−b)2≥0(b^2+c^2-a^2)(b-c)^2+(c^2+a^2-b^2)(c-a)^2+(a^2+b^2-c^2)(a-b)^2\geq 0.

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

View graph