lean_workbook_plus_28716

Disproved

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

prove that: $6abc<ab(a+b)+bc(b+c)+ca(c+a)<2(a^{3}+b^{3}+c^{3})$ where a,b,c>0

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_28716 : ∀ a b c : ℝ, a > 0 ∧ b > 0 ∧ c > 0 → 6 * a * b * c < a * b * (a + b) + b * c * (b + c) + c * a * (c + a) ∧ a * b * (a + b) + b * c * (b + c) + c * a * (c + a) < 2 * (a ^ 3 + b ^ 3 + c ^ 3)   :=  by sorry

Source

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

View graph