lean_workbook_plus_17121Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)Prove that for a,b,c>0a,b,c>0a,b,c>0 from R\mathbb R R and abc=1abc=1abc=1 , we have (a2+1)(b2+1)(c2+1)≥12(abc+1)(a+1)(b+1)(c+1).(a^2+1)(b^2+1)(c^2+1)\ge \frac{1}{2}(abc+1)(a+1)(b+1)(c+1).(a2+1)(b2+1)(c2+1)≥21(abc+1)(a+1)(b+1)(c+1). (a3+1)(b3+1)(c3+1)≥12(abc+1)(a2+1)(b2+1)(c2+1).(a^3+1)(b^3+1)(c^3+1) \ge \frac{1}{2}(abc+1)(a^2+1)(b^2+1)(c^2+1).(a3+1)(b3+1)(c3+1)≥21(abc+1)(a2+1)(b2+1)(c2+1).Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_17121 (a b c : ℝ) (ha : a > 0 ∧ b > 0 ∧ c > 0 ∧ a * b * c = 1) : (a^2 + 1) * (b^2 + 1) * (c^2 + 1) ≥ 1 / 2 * (a * b * c + 1) * (a + 1) * (b + 1) * (c + 1) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph