lean_workbook_plus_81882

Proved

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

$\frac{4}{3} \left( a^2 + 2b^2 + 6ac + 9c^2 \right) = \frac{4}{3} \left( 2b^2 + (a + 3c)^2 \right) \geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_81882 (a b c : ℝ) : (4 / 3) * (a^2 + 2*b^2 + 6*a*c + 9*c^2) = (4 / 3) * (2 * b^2 + (a + 3 * c)^2) ∧ (4 / 3) * (2 * b^2 + (a + 3 * c)^2) ≥ 0   :=  by sorry

Source

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

View graph