lean_workbook_plus_53987

Disproved

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

Given $a, b, c$ are real numbers such that $a + b + c = 3$ , prove that $(3 - a)(3 - b)(3 - c) \geq 8abc$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_53987 : ∀ a b c : ℝ, a + b + c = 3 → (3 - a) * (3 - b) * (3 - c) ≥ 8 * a * b * c   :=  by sorry

Source