lean_workbook_plus_67693Provedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)Let a,b,ca, b, ca,b,c be positive real numbers . Prove that \n\n (a+b)(2b+c)(2c+a)≥12(a+2b+2c)(ab+2bc+2ca)(a+b)(2b+c)(2c+a)\ge \frac{1}{2}(a+2b+2c)(ab+2bc+2ca)(a+b)(2b+c)(2c+a)≥21(a+2b+2c)(ab+2bc+2ca) (a+b)(2b+c)(2c+a)≥13(a+2b+2c)(ab+3bc+3ca)(a+b)(2b+c)(2c+a)\ge \frac{1}{3}(a+2b+2c)(ab+3bc+3ca)(a+b)(2b+c)(2c+a)≥31(a+2b+2c)(ab+3bc+3ca)Preambleimport Mathlib.Analysis.Complex.BasicFormal statementtheorem lean_workbook_plus_67693 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → (a + b) * (2 * b + c) * (2 * c + a) ≥ (1 / 2) * (a + 2 * b + 2 * c) * (a * b + 2 * b * c + 2 * c * a) := by sorrySourcehttps://huggingface.co/datasets/internlm/Lean-WorkbookView graph