Prove2Me

lean_workbook_plus_28226

Disproved

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

We also have: \n

3 4 a2+4 b2+4 c2+6 abc≤15 a3+1+15 b3+1+15 c3+13\,\sqrt {4\,{a}^{2}+4\,{b}^{2}+4\,{c}^{2}+6\,abc}\leq \sqrt {15\,{a}^{3}+1}+\sqrt {15\,{b}^{3}+1}+\sqrt {15\,{c}^{3}+1}
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_28226 :  ∀ a b c : ℝ, 3 * Real.sqrt (4 * a ^ 2 + 4 * b ^ 2 + 4 * c ^ 2 + 6 * a * b * c) ≤ Real.sqrt (15 * a ^ 3 + 1) + Real.sqrt (15 * b ^ 3 + 1) + Real.sqrt (15 * c ^ 3 + 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph