lean_workbook_plus_73212

Proved

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

$(bc^3+ca^3+ab^3)^2\geq 3abc(a^2c^3+a^3b^2+b^3c^2).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73212 (a b c : ℝ) : (b * c ^ 3 + c * a ^ 3 + a * b ^ 3) ^ 2 ≥ 3 * a * b * c * (a ^ 2 * c ^ 3 + a ^ 3 * b ^ 2 + b ^ 3 * c ^ 2)   :=  by sorry

Source

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

View graph