lean_workbook_plus_14251

Disproved

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

For $a,b,c \in \mathbb{R}$ so that $a+b+c=1$ Prove that $ab(3a-1)+ac(3b-1)+bc(3c-1) \geq 0$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_14251 : ∀ a b c : ℝ, a + b + c = 1 → a * b * (3 * a - 1) + a * c * (3 * b - 1) + b * c * (3 * c - 1) ≥ 0   :=  by sorry

Source