lean_workbook_plus_18428

Proved

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

Prove: $LHS-RHS=(1/126)*(21*a^2+7*a*b-17*a*c-21*b^2+10*b*c)^2+(1/126)*(-17*a*b+10*a*c+21*b^2+7*b*c-21*c^2)^2+(1/126)*(-21*a^2+10*a*b+7*a*c-17*b*c+21*c^2)^2+(263/9198)*(7*a*b-17*a*c+10*b*c)^2+(263/9198)*(-17*a*b+10*a*c+7*b*c)^2+(263/9198)*(10*a*b+7*a*c-17*b*c)^2\ge 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18428 {a b c : ℝ} :
  (1 / 126) * (21 * a ^ 2 + 7 * a * b - 17 * a * c - 21 * b ^ 2 + 10 * b * c) ^ 2 + (1 / 126) * (-17 * a * b + 10 * a * c + 21 * b ^ 2 + 7 * b * c - 21 * c ^ 2) ^ 2 + (1 / 126) * (-21 * a ^ 2 + 10 * a * b + 7 * a * c - 17 * b * c + 21 * c ^ 2) ^ 2 + (263 / 9198) * (7 * a * b - 17 * a * c + 10 * b * c) ^ 2 + (263 / 9198) * (-17 * a * b + 10 * a * c + 7 * b * c) ^ 2 + (263 / 9198) * (10 * a * b + 7 * a * c - 17 * b * c) ^ 2 ≥ 0   :=  by sorry

Source

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

View graph