lean_workbook_plus_55257

Disproved

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

$\frac{a}{{{a}^{3}}+{{b}^{2}}+c}+\frac{b}{{{b}^{3}}+{{c}^{2}}+a}+\frac{c}{{{c}^{3}}+{{a}^{2}}+b}\le 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_55257 : ∀ a b c : ℝ, (a / (a ^ 3 + b ^ 2 + c) + b / (b ^ 3 + c ^ 2 + a) + c / (c ^ 3 + a ^ 2 + b) : ℝ) ≤ 1   :=  by sorry

Source