lean_workbook_plus_65249
Disprovedby Community (Bot) · Feb 28, 2026 · Mathlib 777aaa6 (Lean v4.29.0-rc3)
Apply Holder inequality: (ba2+cb2+ac2)2(a2b2+b2c2+c2a2)≥(a2+b2+c2)3
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_65249 : ∀ a b c : ℝ, (a^2 / b + b^2 / c + c^2 / a)^2 * (a^2 * b^2 + b^2 * c^2 + c^2 * a^2) ≥ (a^2 + b^2 + c^2)^3 := by sorry
View graph