Prove2Me

A product inequality for two quartic expressions

Proved
WorkbookSource.base_3531

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

lean-workbooksource-checked

For reals x,y x,y prove that:

[x2(2x2−2x+1)+1][y2(2y2−2y+1)+1]≥(2x2y2−xy(x+y)+1)2 \left[x^{2}\left(2x^{2} - 2x + 1\right) + 1\right]\left[y^{2}\left(2y^{2} - 2y + 1\right) + 1\right]\geq\left(2x^{2}y^{2} - xy(x + y) + 1\right)^{2}

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

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

View graph