Prove2Me

lean_workbook_plus_19344

Disproved

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

=(a+b+c)43abc(a+b+c)≥(a+b+c)4(ab+bc+ca)2≥3(a+b+c)2ab+bc+ca=\frac{(a+b+c)^{4}}{3abc(a+b+c)}\geq \frac{(a+b+c)^{4}}{(ab+bc+ca)^{2}}\geq \frac{3(a+b+c)^{2}}{ab+bc+ca}

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

View graph