lean_workbook_plus_64511

Proved

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

Let $a,$ $b$ and $c$ are positive real numbers, such that $abc=1.$ Prove that $a^2+b^2+c^2+ab+ac+bc+6\geq4(a+b+c).$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64511 (a b c : ℝ) (h : a * b * c = 1) :
  a^2 + b^2 + c^2 + a * b + b * c + a * c + 6 ≥ 4 * (a + b + c)   :=  by sorry

Source