Prove2Me

lean_workbook_plus_82423

Proved

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

Prove that for all reals aa, bb, and cc, if k≥27163k \geq \sqrt[3]{\frac{27}{16}}, then ka3−abc3+kb3−abc3+kc3−abc3≥0\sqrt[3]{ka^3-abc}+\sqrt[3]{kb^3-abc}+\sqrt[3]{kc^3-abc}\geq 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_82423 (a b c k : ℝ) (h₁ : k ≥ (27 / 16)^(1 / 3)) : (k * a ^ 3 - a * b * c) ^ (1 / 3) + (k * b ^ 3 - a * b * c) ^ (1 / 3) + (k * c ^ 3 - a * b * c) ^ (1 / 3) ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph