lean_workbook_plus_26468

Proved

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

Let $a,b,c,d>0$ . Prove that:

\frac{a}{\sqrt{a+b}}+\frac{b}{\sqrt{b+c}}+\frac{c}{\sqrt{c+d}}+\frac{d}{\sqrt{d+a}}\leq \sqrt {a}+\sqrt {b}+\sqrt {c}+\sqrt {d}

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_26468 (a b c d : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) : (a / Real.sqrt (a + b) + b / Real.sqrt (b + c) + c / Real.sqrt (c + d) + d / Real.sqrt (d + a)) ≤ Real.sqrt a + Real.sqrt b + Real.sqrt c + Real.sqrt d   :=  by sorry

Source

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

View graph