lean_workbook_plus_78369

Proved

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

$(a^2+b^2+c^2 )(a^2b^2+b^2c^2+c^2a^2)\stackrel {am-gm}{\geq} 9a^2b^2c^2=9(4R\triangle)^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_78369 (a b c : ℝ) (hab : a > 0 ∧ b > 0 ∧ c > 0) (habc : a + b > c) (hbc : b + c > a) (hca : a + c > b) : (a^2 + b^2 + c^2) * (a^2 * b^2 + b^2 * c^2 + c^2 * a^2) ≥ 9 * a^2 * b^2 * c^2   :=  by sorry

Source

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

View graph