lean_workbook_plus_33786

Proved

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

Prove the identity: $a+b+c=2p\Longrightarrow \sum a(p-b)(p-c)(b^{2}-c^{2})=-p^{2}(a-b)(b-c)(c-a)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_33786 {a b c p : ℝ} (h : a + b + c = 2 * p) :
  a * (p - b) * (p - c) * (b ^ 2 - c ^ 2) + b * (p - c) * (p - a) * (c ^ 2 - a ^ 2) +
      c * (p - a) * (p - b) * (a ^ 2 - b ^ 2) = -p ^ 2 * (a - b) * (b - c) * (c - a)   :=  by sorry

Source

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

View graph