lean_workbook_plus_61257

Proved

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

Prove that $9(a^6 + b^6 + c^6) + 6a^2b^2c^2 \geq 7(a^3b^3 + b^3c^3 + c^3a^3) + 4abc(a^3 + b^3 + c^3)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_61257 (a b c : ℝ) : 9 * (a ^ 6 + b ^ 6 + c ^ 6) + 6 * a ^ 2 * b ^ 2 * c ^ 2 ≥ 7 * (a ^ 3 * b ^ 3 + b ^ 3 * c ^ 3 + c ^ 3 * a ^ 3) + 4 * a * b * c * (a ^ 3 + b ^ 3 + c ^ 3)   :=  by sorry

Source

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

View graph