Prove2Me

A triangle semiperimeter-weighted difference inequality

Proved
WorkbookSource.plus_61196

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

For a triangle with sides a,b,ca,b,c and semi-perimeter ss , prove that:

(s−a)(b−c)2+(s−b)(c−a)2+(s−c)(a−b)2≤abc(s-a)(b-c)^2 + (s-b)(c-a)^2 + (s-c)(a-b)^2 \leq abc

Source: InternLM Lean-Workbook, record lean_workbook_plus_61196 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.plus_61196 {a b c s : ℝ} (hx: a + b + c = 2 * s) (hab : a + b > c) (hbc : b + c > a) (hca : a + c > b) : (s - a) * (b - c) ^ 2 + (s - b) * (c - a) ^ 2 + (s - c) * (a - b) ^ 2 ≤ a * b * c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_61196; Apache-2.0

View graph