Prove2Me

lean_workbook_plus_1534

Proved

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

By AM-GM, we have ab+bc+ac≥3a2b2c23ab+bc+ac\geq3\sqrt[3]{a^2b^2c^2} and also ab+bc+ac≥3abc3\sqrt{ab}+\sqrt{bc}+\sqrt{ac}\geq3\sqrt[3]{abc}. Therefore the desired inequality becomes 27(abc)43≥2727\sqrt[3]{(abc)^4}\geq27. It remains to show that abc≥1abc\geq 1 .

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

View graph