Prove2Me

lean_workbook_plus_16855

Proved

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

Let aa , bb , cc be real numbers such that 0<a≤b≤c0 < a \le b \le c . Prove that (a+3b)(b+4c)(c+2a)≥60abc(a + 3b)(b + 4c)(c + 2a) \ge 60abc . When does equality hold?

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_16855 (a b c : ℝ) (h₀ : 0 < a ∧ 0 < b ∧ 0 < c) (h₁ : a ≤ b ∧ b ≤ c) : (a + 3 * b) * (b + 4 * c) * (c + 2 * a) ≥ 60 * a * b * c   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph