lean_workbook_plus_73699

Disproved

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

For $ab+bc+ca=3$ the following inequalities holds:\n\n1) $a^2 + b^2 + c^2 + 3abc\ge 6$ (Vasc's inequality)\n\n2) $a^2 + b^2 + c^2\ge a + b + c$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_73699 :  ∀ a b c : ℝ, a * b + b * c + c * a = 3 → a ^ 2 + b ^ 2 + c ^ 2 + 3 * a * b * c ≥ 6   :=  by sorry

Source