Prove2Me

lean_workbook_plus_34086

Disproved

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

(b) Prove that the polynomial z2(x2−y2)(x2−1)+y2(y2−x2)(y2−1)+(1−x2)(1−y2)z^2(x^2-y^2)(x^2-1)+ y^2(y^2-x^2)(y^2-1)+(1-x^2)(1-y^2) is every where nonnegetive, but cannot be written as the sum of squares of any number of polynomials.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_34086 : ∀ x y z : ℝ, (z^2 * (x^2 - y^2) * (x^2 - 1) + y^2 * (y^2 - x^2) * (y^2 - 1) + (1 - x^2) * (1 - y^2)) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph