lean_workbook_plus_73296

Proved

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

Prove that $7(\sum_{cyc}a^6)+21a^2b^2c^2\geq 14(\sum_{cyc}a^4bc)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73296 (a b c : ℝ) : 7 * (a ^ 6 + b ^ 6 + c ^ 6) + 21 * a ^ 2 * b ^ 2 * c ^ 2 ≥ 14 * (a ^ 4 * b * c + b ^ 4 * c * a + c ^ 4 * a * b)   :=  by sorry

Source

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

View graph