lean_workbook_plus_40803

Proved

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

Prove that $2(a^2+b^2)(b^2+c^2)(c^2+a^2)\ge\((a+b)(b+c)(c+a)-4abc)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_40803 (a b c : ℝ) :
  2 * (a^2 + b^2) * (b^2 + c^2) * (c^2 + a^2) ≥ ((a + b) * (b + c) * (c + a) - 4 * a * b * c)^2   :=  by sorry

Source

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

View graph