Prove2Me

lean_workbook_plus_31005

Proved

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

from ab+bc+ac+2abc=1ab+bc+ac+2abc=1, by AM-GM, 1−2abc=ab+bc+ac≥3(abc)231-2abc =ab+bc+ac \ge 3(abc)^{\frac{2}{3}}. Then set (abc)13=x(abc)^{\frac{1}{3}}=x. We have 1−2x3≥3x2  ⟹  (x+1)2(2x−1)≤01-2x^3 \ge 3x^2 \implies (x+1)^2(2x-1) \le 0. Draw a graph of f(x)=(x+1)2(2x−1)f(x)=(x+1)^2(2x-1) and we will see x≤12x\le \frac{1}{2}, i.e. abc≤18abc \le \frac{1}{8}.

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

View graph