Prove2Me

An asymmetric cubic polynomial is nonnegative

Proved
WorkbookSource.base_8207

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

lean-workbooksource-checked

Show the steps to prove the inequality 4x3+(−4z−4y)x2+(6yz−z2−y2)x+3(y+z)(y−z)2≥04x^3+(-4z-4y)x^2+(6yz-z^2-y^2)x+3(y+z)(y-z)^2\ge 0 for positive reals x, y, and z.

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

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

View graph