lean_workbook_plus_7820

Proved

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

we have $a^3\geq a^2$ and $b^3\geq b^2$ and $c^3\geq c^2$ because $a,b,c\geq 1$ then $a^3+b^3+c^3\geq a^2+b^2+c^2$ and from Am-Gm $a+b+c\geq 3\sqrt[3]{abc}\geq 3$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_7820  (a b c : ℝ)
  (h₀ : 1 ≤ a ∧ 1 ≤ b ∧ 1 ≤ c) :
  a^3 + b^3 + c^3 ≥ a^2 + b^2 + c^2   :=  by sorry

Source

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

View graph