A reciprocal four-variable product bounds a cyclic ratio sum at fixed total four

Proved

WorkbookSource.base_10302

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

lean-workbooksource-checked

If $a+b+c+d=4$ and $a,b,c,d >0$ , prove that $\frac {4} {abcd} \ge \frac {a} {b}+ \frac {b} {c} + \frac {c} {d} +\frac {d} {a}$ .

Source: InternLM Lean-Workbook, record lean_workbook_10302 (Apache-2.0). Complete source proposition preserved; proof developed independently.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.base_10302 (a b c d : ℝ) (hab : 0 < a) (hbc : 0 < b) (hcd : 0 < c) (hda : 0 < d)  (habcd : a + b + c + d = 4) : 4 / (a * b * c * d) ≥ a / b + b / c + c / d + d / a  :=  by sorry

Source

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

View graph