Prove2Me

lean_workbook_plus_65686

Proved

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

For a,b,ca,b,c sides of a triangle prove that (a+b+c)3≥(5a−b−c)(5b−c−a)(5c−a−b)(a+b+c)^3 \geq (5a-b-c)(5b-c-a)(5c-a-b)

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65686 {a b c : ℝ} (hx: a > 0 ∧ b > 0 ∧ c > 0) (hab : a + b > c) (hbc : b + c > a) (hca : a + c > b) : (a + b + c) ^ 3 >= (5 * a - b - c) * (5 * b - c - a) * (5 * c - a - b)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph