lean_workbook_plus_34544

Proved

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

The following inequality is true? $3853\,{y}^{8}-17894\,{y}^{7}z+44839\,{y}^{6}{z}^{2}-74828\,{y}^{5}{z}^{3}+88465\,{y}^{4}{z}^{4}-74828\,{y}^{3}{z}^{5}+44839\,{y}^{2}{z}^{6}-17894\,y{z}^{7}+3853\,{z}^{8} \geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34544 (y z : ℝ) : 3853*y^8 - 17894*y^7*z + 44839*y^6*z^2 - 74828*y^5*z^3 + 88465*y^4*z^4 - 74828*y^3*z^5 + 44839*y^2*z^6 - 17894*y*z^7 + 3853*z^8 ≥ 0   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph