A cyclic product bound under unit product

Proved

WorkbookCorrected.base_44343

by wamlart · Sep 13, 2026 · Mathlib 0df444a (Lean v4.33.1)

corrected-formalizationlean-workbooksource-checked

Let $a,b, c$ real positive numbers such that $abc=1$ .Prove that $a^2b(b^3-1)+b^2c(c^3-1)+c^2a(a^3-1)\ge 0.$

Source: InternLM Lean-Workbook, record lean_workbook_44343 (Apache-2.0). Natural-language proposition preserved; missing source domain assumptions restored. Proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookCorrected.base_44343 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (h : a * b * c = 1) :  a^2 * b * (b^3 - 1) + b^2 * c * (c^3 - 1) + c^2 * a * (a^3 - 1) ≥ 0  :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_44343; Apache-2.0

View graph