lean_workbook_plus_34269

Proved

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

Prove that, $(a+3b)(b+4c)(c+2a) \geq 60abc$ for all real numbers $0\leq a\leq b\leq c$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34269 : ∀ a b c : ℝ, 0 ≤ a ∧ a ≤ b ∧ b ≤ c → (a + 3 * b) * (b + 4 * c) * (c + 2 * a) ≥ 60 * a * b * c   :=  by sorry

Source