lean_workbook_plus_18949

Proved

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

Given $a+b+c=a^3+b^3+c^3=1$ and $a, b, c$ are real numbers, prove that $(ab+bc+ca)^3=a^3b^3+b^3c^3+c^3a^3$ using the identity $(x+y+z)^3=x^3+y^3+z^3+3(x+y+z)(xy+yz+xz)-3xyz$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_18949 (a b c : ℝ) (h₁ : a + b + c = 1) (h₂ : a^3 + b^3 + c^3 = 1) : (a * b + b * c + c * a)^3 = a^3 * b^3 + b^3 * c^3 + c^3 * a^3   :=  by sorry

Source

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

View graph