Prove2Me

lean_workbook_plus_8058

Proved

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

Let a≥4,b,c≥0,a+b≤2c,x,y,z∈Ra\geq 4,b,c\geq 0,a+b\leq 2c,x,y,z\in R. Prove that (a−3)(b−x2−y2−z2)≤(c−x−y−z)2.(a-3)(b-x^2-y^2-z^2)\leq (c-x-y-z)^2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_8058 (a b c x y z : ℝ) (ha : a ≥ 4) (hb : b ≥ 0) (hc : c ≥ 0) (hab : a + b ≤ 2 * c) : (a - 3) * (b - x ^ 2 - y ^ 2 - z ^ 2) ≤ (c - x - y - z) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph