Prove2Me

lean_workbook_plus_1269

Disproved

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

P3 abc(a+b+c−2)≥2(1−3abc−(bc)3−(ca)3−(ab)3)a+b+c\sqrt{abc}(a+b+c-2)\ge \frac{2\left(1-3abc-\left(\sqrt{bc}\right)^3-\left(\sqrt{ca}\right)^3-\left(\sqrt{ab}\right)^3\right)}{\sqrt{a}+\sqrt{b}+\sqrt{c}}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_1269 : ∀ a b c : ℝ, (Real.sqrt a * Real.sqrt b * Real.sqrt c) * (a + b + c - 2) ≥ (2 * (1 - 3 * a * b * c - (Real.sqrt (b * c))^3 - (Real.sqrt (c * a))^3 - (Real.sqrt (a * b))^3)) / (Real.sqrt a + Real.sqrt b + Real.sqrt c)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph