lean_workbook_plus_56791

Disproved

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

From schur inequality we have : $(a+b+c)^3+9abc \ge 4(a+b+c)(ab+bc+ca)$ , so if $a+b+c=1$ we get \n $4(ab+bc+ca)-9abc \le 1$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_56791 : ∀ a b c : ℝ, a + b + c = 1 → 4 * (a * b + b * c + c * a) - 9 * a * b * c ≤ 1   :=  by sorry

Source