Prove2Me

lean_workbook_plus_78959

Proved

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

Let k=a+b+ck=a+b+c. Then 3(a2+b2+c2)−2(ab+bc+ca+a+b+c)=4(a2+b2+c2)−k(k+2)3(a^2 + b^2 + c^2) - 2(ab + bc + ca + a + b + c) = 4(a^2 + b^2 + c^2) - k(k+2) But, by power means, this is greater than or equal to 43(a+b+c)2−k(k+2) = 13(k−3)2−3 ≥ −3\tfrac{4}{3}(a+b+c)^2 -k(k+2) \,=\, \tfrac{1}{3}(k-3)^2-3 \,\ge\, {\bf -3} and that bound is attained for a=b=c=k3=1■a=b=c=\tfrac{k}{3}=1\quad\blacksquare

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

View graph