lean_workbook_plus_69921

Proved

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

$27a^{2}b^{2}c^{2}\ge\prod ( 2b^{2}+2c^{2}-a^{2})\Leftrightarrow \sum (b^{2}+c^{2}-2a^{2})(b^{2}-c^{2})^{2}\ge0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_69921 (a b c : ℝ) : 27 * a ^ 2 * b ^ 2 * c ^ 2 ≥ (2 * b ^ 2 + 2 * c ^ 2 - a ^ 2) * (2 * c ^ 2 + 2 * a ^ 2 - b ^ 2) * (2 * a ^ 2 + 2 * b ^ 2 - c ^ 2) ↔ (b ^ 2 + c ^ 2 - 2 * a ^ 2) * (b ^ 2 - c ^ 2) ^ 2 + (c ^ 2 + a ^ 2 - 2 * b ^ 2) * (c ^ 2 - a ^ 2) ^ 2 + (a ^ 2 + b ^ 2 - 2 * c ^ 2) * (a ^ 2 - b ^ 2) ^ 2 ≥ 0   :=  by sorry

Source

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

View graph