Prove2Me

Factoring a cyclic cubic expression

Proved
WorkbookSource.problem_23797

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

lean-workbooksource-checked

∑cyc4x3−4x2+x≥0⟺∑cycx(2x−1)2≥0\sum_{cyc}{4x^3-4x^2+x} \ge 0 \Longleftrightarrow \sum_{cyc}{x(2x-1)^2} \ge 0

Source: InternLM Lean-Workbook, record lean_workbook_23797 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

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

View graph