lean_workbook_plus_60274

Disproved

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

$x^{3}+y^{3}\ge x^{2}y+xy^{2};x^{3}+y^{3}+z^{3}\ge xy^{2}+yz^{2}+zx^{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60274 : ∀ x y : ℝ, x ^ 3 + y ^ 3 ≥ x ^ 2 * y + x * y ^ 2 ∧ ∀ x y z : ℝ, x ^ 3 + y ^ 3 + z ^ 3 ≥ x * y ^ 2 + y * z ^ 2 + z * x ^ 2   :=  by sorry

Source

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

View graph