lean_workbook_plus_36993

Proved

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

Suppose that positive numbers $x$ and $y$ satisfy $x^2+y^3+z^4 \geqslant x^3+y^4+z^5.$ Prove that $x^3+y^3+z^3 \leqslant 3.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_36993 (x y z : ℝ) (hx: 0 < x) (hy: 0 < y) (hz: 0 < z) (h : x^2 + y^3 + z^4 ≥ x^3 + y^4 + z^5) : x^3 + y^3 + z^3 ≤ 3   :=  by sorry

Source

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

View graph