lean_workbook_plus_52027

Proved

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

Your inequality is linear of $abc$ . Hence, by $uvw$ we need to check two cases: 1. $abc\rightarrow0^+$ . In this case our inequality is obviously true; 2. $b=c=1$ , which gives $(a+2)^8\geq243(2a^2+1)(2a+1)^2$ . The last inequality we can prove by calculus.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_52027  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a * b * c = 1) :
  (a + 2)^8 ≥ 243 * (2 * a^2 + 1) * (2 * a + 1)^2   :=  by sorry

Source

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

View graph