lean_workbook_plus_60300

Disproved

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

Given $a, b, c \geq\ 0$ satisfy $ab + bc + ca = 3$ . Prove that: $\sqrt [3]{5a^3 + 3a} + \sqrt [3]{5b^3 + 3b} + \sqrt [3]{5c^3 + 3c} \geq\ 6$ . PS: It exitst an easy proof by Am-Gm, my friend

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60300 (a b c : ℝ) (ha : a ≥ 0) (hb : b ≥ 0) (hc : c ≥ 0) (hab : a * b + b * c + c * a = 3) : (5 * a ^ 3 + 3 * a) ^ (1 / 3) + (5 * b ^ 3 + 3 * b) ^ (1 / 3) + (5 * c ^ 3 + 3 * c) ^ (1 / 3) ≥ 6   :=  by sorry

Source

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

View graph