lean_workbook_plus_23336

Proved

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

If $x,y,z$ are real numbers so that $x+y+z=0$ , prove that $\frac{x^2+y^2+z^2}{2}\frac{x^5+y^5+z^5}{5}=\frac{x^7+y^7+z^7}{7}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_23336 (x y z : ℝ) (h : x + y + z = 0) :
  (x^2 + y^2 + z^2) / 2 * (x^5 + y^5 + z^5) / 5 = (x^7 + y^7 + z^7) / 7   :=  by sorry

Source

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

View graph