lean_workbook_plus_49238

Proved

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

First, we have $(a^2+b^2)(b^2+c^2)(c^2+a^2) \ge \frac{1}{2}[(a+b)(b+c)(c+a)-4abc]^2. \quad (1)$ It's by Cauchy-Schwarz.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_49238 : ∀ a b c : ℝ, (a^2 + b^2) * (b^2 + c^2) * (c^2 + a^2) ≥ (1/2)*((a + b) * (b + c) * (c + a) - 4 * a * b * c)^2   :=  by sorry

Source

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

View graph