lean_workbook_plus_79131

Disproved

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

Vasc had a stronger inequality: $\frac{a^5}{a^4+b^4}+\frac{b^5}{b^4+c^4}+\frac{c^5}{c^4+a^4} \ge \frac{1}{2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_79131 : ∀ a b c : ℝ, (a ^ 5 / (a ^ 4 + b ^ 4) + b ^ 5 / (b ^ 4 + c ^ 4) + c ^ 5 / (c ^ 4 + a ^ 4)) ≥ 1 / 2   :=  by sorry

Source