lean_workbook_plus_45580

Proved

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

Prove that $(a+d)^2+(b+e)^2+(c+f)^2 \ge \sum_{sym}ab=(a+d)(b+e)+(b+e)(c+f)+(c+f)(a+d)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45580 (a b c d e f : ℝ) : (a + d) ^ 2 + (b + e) ^ 2 + (c + f) ^ 2 ≥ (a + d) * (b + e) + (b + e) * (c + f) + (c + f) * (a + d)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph