lean_workbook_plus_4307

Disproved

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

Inequality 2:\nBy Cauchy Schwarz $\sum \frac{4a}{b+c}\leq \sum (\frac{a}{b}+\frac{a}{c})\Rightarrow$ we need to prove: \n\n $\frac{a^3+b^3+c^3}{abc}\geq \frac{a}{b}+\frac{b}{c}+\frac{c}{a}\Leftrightarrow a^3+b^3+c^3\geq a^2c+b^2a+c^2b$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4307 : ∀ a b c : ℝ, a * b * c > 0 → a^3 + b^3 + c^3 ≥ a^2 * c + b^2 * a + c^2 * b   :=  by sorry

Source

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

View graph