lean_workbook_plus_1810

Proved

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

The following inequality is also true. \nIf $a, b, c>0, abc=1$ prove that \n $\sum_{cyc}{\\frac{1}{(2a^3+1)(a^3+2)}}\\ge\\frac{1}{3}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1810 (a b c : ℝ) (ha : a > 0 ∧ b > 0 ∧ c > 0 ∧ a * b * c = 1) : 1 / (2 * a ^ 3 + 1) * (a ^ 3 + 2) + 1 / (2 * b ^ 3 + 1) * (b ^ 3 + 2) + 1 / (2 * c ^ 3 + 1) * (c ^ 3 + 2) ≥ 1 / 3   :=  by sorry

Source

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

View graph