Prove2Me

lean_workbook_plus_68861

Proved

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

Prove that: x3+y3+z3+t3≥12 x^3+y^3+z^3+t^3\geq \frac{1}{2} given (x;y;z;t)∈R(x;y;z;t) \in R such as x≥−1 x\geq-1 ; y≥−1 y\geq-1 ; z≥−1 z\geq-1 ; t≥−1 t\geq-1 and x+y+z+t=2 x+y+z+t=2

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_68861 (x y z t : ℝ) (hx : x ≥ -1) (hy : y ≥ -1) (hz : z ≥ -1) (ht : t ≥ -1) (h : x + y + z + t = 2) : x ^ 3 + y ^ 3 + z ^ 3 + t ^ 3 ≥ 1 / 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph