A cyclic inequality between three quadratic products

Proved

WorkbookSource.problem_6826

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

Let $a,$ $b,$ $c$ be real numbers. Prove that $\begin{aligned} (a^2 + 2ab & + 3b^2)(b^2 + 2bc + 3c^2)(c^2 + 2ca + 3a^2) \ge & \ge 8(a^2 + ab + bc)(b^2 + bc + ca)(c^2 + ca + ab).\end{aligned}$

Source: InternLM Lean-Workbook, record lean_workbook_6826 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.problem_6826 (a b c : ℝ) : (a^2 + 2 * a * b + 3 * b^2) * (b^2 + 2 * b * c + 3 * c^2) * (c^2 + 2 * c * a + 3 * a^2) ≥ 8 * (a^2 + a * b + b * c) * (b^2 + b * c + c * a) * (c^2 + c * a + a * b)  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_6826; Apache-2.0

View graph