lean_workbook_plus_45523

Proved

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

Check the cases $x,y,z\in \{0,1\}$ for the inequality $x^2+y^2+z^2\le x^2y+y^2z+z^2x+1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_45523 (x y z : ℕ) (hx : x = 0 ∨ x = 1) (hy : y = 0 ∨ y = 1) (hz : z = 0 ∨ z = 1) : x^2 + y^2 + z^2 ≤ x^2 * y + y^2 * z + z^2 * x + 1   :=  by sorry

Source

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

View graph