A cyclic difference bound under unit product

Proved

WorkbookCorrected.plus_76029

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

corrected-formalizationlean-workbooksource-checked

Prove or disprove: if positive real numbers $a, b, c$ satisfy that $abc = 1$ , then $\sum (ab - 1)^{2} + \sum(1 - c)^{2} \geq \sum ab(a - b)$

Source: InternLM Lean-Workbook, record lean_workbook_plus_76029 (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.plus_76029 (a b c : ℝ) (source_domain_a : 0 < a) (source_domain_b : 0 < b) (source_domain_c : 0 < c) (h : a * b * c = 1) :
  (a * b - 1) ^ 2 + (b * c - 1) ^ 2 + (c * a - 1) ^ 2 + (1 - a) ^ 2 + (1 - b) ^ 2 + (1 - c) ^ 2 ≥ a * b * (a - b) + b * c * (b - c) + c * a * (c - a)   :=  by sorry

Source

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

View graph