lean_workbook_plus_48129

Disproved

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

Because $(a+b)(b+c)(c+a)\ge\frac{8(a+b+c)(ab+bc+ca)}{9}$ \nfrom it result $a^2+b^2+c^2+\frac{9abc}{a+b+c}\ge 2(ab+bc+ca)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_48129 :
  ∀ a b c : ℝ, a^2 + b^2 + c^2 + (9 * a * b * c) / (a + b + c) ≥ 2 * (a * b + b * c + c * a)   :=  by sorry

Source