lean_workbook_plus_21310

Disproved

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

Prove that $1\ge{a^2+b^2+c^2}\ge{a^2b+b^2c+c^2a}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_21310 : ∀ a b c : ℝ, 1 ≥ a ^ 2 + b ^ 2 + c ^ 2 ∧ a ^ 2 + b ^ 2 + c ^ 2 ≥ a ^ 2 * b + b ^ 2 * c + c ^ 2 * a   :=  by sorry

Source