Prove2Me

lean_workbook_plus_76873

Proved

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

  ⟺  (a+d)2+(b+e)2+(c+f)2≥(a+d)(b+e)+(a+d)(c+f)+(b+e)(c+f)\iff (a+d)^2+(b+e)^2+(c+f)^2\ge (a+d)(b+e)+(a+d)(c+f)+(b+e)(c+f)
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_76873 (a b c d e f : ℝ) : (a+d)^2+(b+e)^2+(c+f)^2 ≥ (a+d)*(b+e)+(a+d)*(c+f)+(b+e)*(c+f)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph