Prove2Me

Quadratic factors bound a Vandermonde product

Proved
WorkbookSource.base_29370

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

lean-workbooksource-checked

Prove that ∑cyc(y−z)2(x2−x+1)≥3(x−y)(y−z)(z−x)\sum_{cyc} (y-z)^2(x^2-x+1) \geq 3(x-y)(y-z)(z-x)

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

Preamble
import Mathlib
open Real Nat
Formal statement
theorem WorkbookSource.base_29370 (x y z : ℝ) : (y - z) ^ 2 * (x ^ 2 - x + 1) + (z - x) ^ 2 * (y ^ 2 - y + 1) + (x - y) ^ 2 * (z ^ 2 - z + 1) ≥ 3 * (x - y) * (y - z) * (z - x)  :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_29370; Apache-2.0

View graph