lean_workbook_plus_31926

Proved

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

Prove that $\sum_\text{cyc} \frac{2ab-a^2 - b^2}{a^2 + b^2 + 2 c^2} = \sum_\text{cyc} \frac{-(a-b)^2}{a^2 + b^2 + 2 c^2} \le 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31926 (a b c : ℝ) :
  (2 * a * b - a ^ 2 - b ^ 2) / (a ^ 2 + b ^ 2 + 2 * c ^ 2) +
    (2 * b * c - b ^ 2 - c ^ 2) / (b ^ 2 + c ^ 2 + 2 * a ^ 2) +
      (2 * c * a - c ^ 2 - a ^ 2) / (c ^ 2 + a ^ 2 + 2 * b ^ 2) ≤
    0   :=  by sorry

Source

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

View graph