lean_workbook_plus_31579

Proved

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

Let $x+y+z=T_1; xy+yz+zx=T_2; xyz=T_3$ . Prove that $(x-y)^2(y-z)^2(z-x)^2=T_1^2T_2^2 + 18{T_1}{T_2}{T_3} - 4T_1^3{T_3} - 4T_2^3 - 27T_3^2.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_31579 {x y z T1 T2 T3 : ℝ} (hx : x + y + z = T1) (hy : x*y + y*z + z*x = T2) (hz : x*y*z = T3) : (x - y) ^ 2 * (y - z) ^ 2 * (z - x) ^ 2 = T1 ^ 2 * T2 ^ 2 + 18*T1*T2*T3 - 4*T1 ^ 3 * T3 - 4*T2 ^ 3 - 27*T3 ^ 2   :=  by sorry

Source

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

View graph