Prove2Me

lean_workbook_plus_54450

Proved

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

Prove that \n (a2+b2)(b2+c2)(c2+a2)≥2(ab2+bc2+ca2−abc)(a2b+b2c+c2a−abc)(a^2+b^2)(b^2+c^2)(c^2+a^2)\geq 2(ab^2+bc^2+ca^2-abc)(a^2b+b^2c+c^2a-abc)

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

View graph