Prove2Me

lean_workbook_plus_79770

Proved

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

Let a,b,c a,b,c be positive numbers such that abc≥1 abc \ge 1 \nProve that a3+b3+c3≥ab+bc+ca a^3 + b^3 + c^3\ge ab + bc + ca \nWe can use AM-GM \n a3+b3+1≥3ab,b3+c3+1≥3bc,c3+a3+1≥3ca a^3+b^3+1 \ge 3ab ,b^3+c^3+1 \ge 3bc, c^3+a^3+1 \ge 3ca \nand ab+bc+ca≥3 ab+bc+ca \ge 3

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_79770  (a b c : ℝ)
  (h₀ : 0 < a ∧ 0 < b ∧ 0 < c)
  (h₁ : a * b * c ≥ 1) :
  a^3 + b^3 + c^3 ≥ a * b + b * c + c * a   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph