lean_workbook_plus_7857

Proved

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

The following inequality holds for any triangle with sides $a,b,c$ \n $a(b^2+c^2-a^2)+b(c^2+a^2-b^2)+c(a^2+b^2-c^2)<= 3abc$ \n if we simplify this, we get \n $(a+b)(a-b)^2+(b+c)(b-c)^2+(c+a)(c-a)^2>= (a+b+c)(a^2+b^2+c^2-ab-bc-ca)$ \n I used Chebyshev inequality here...\n\nBut the answer uses cosine law and blah blah..\nIs my idea correct? Thanks in advance.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7857 :
  ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 ∧ a + b > c ∧ a + c > b ∧ b + c > a → a * (b^2 + c^2 - a^2) + b * (c^2 + a^2 - b^2) + c * (a^2 + b^2 - c^2) ≤ 3 * a * b * c   :=  by sorry

Source

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

View graph