lean_workbook_plus_55751

Disproved

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

Squaring both sides, we have: $ab(a+b) + bc(b+c) + ca(c+a) + 2\sqrt{a^2bc(a+b)(a+c)} + 2\sqrt{ab^2c(b+a)(b+c)} + 2\sqrt{abc^2(c+a)(c+b)}\geq 4abc + (a+b)(b+c)(c+a)$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55751 : ∀ a b c : ℝ, a * b * (a + b) + b * c * (b + c) + c * a * (c + a) + 2 * Real.sqrt (a ^ 2 * b * c * (a + b) * (a + c)) + 2 * Real.sqrt (a * b ^ 2 * c * (b + a) * (b + c)) + 2 * Real.sqrt (a * b * c ^ 2 * (c + a) * (c + b)) ≥ 4 * a * b * c + (a + b) * (b + c) * (c + a)   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook

View graph