lean_workbook_plus_32961

Proved

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

For 6 variables, if $a,b,c,d,e,f$ are positive reals, then $\frac{ab}{a+b}+\frac{cd}{c+d}+\frac{ef}{e+f} \le \frac{(a+c+e)(b+d+f)}{a+b+c+d+e+f}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_32961 (a b c d e f : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) (hd : 0 < d) (he : 0 < e) (hf : 0 < f) : (a * b / (a + b) + c * d / (c + d) + e * f / (e + f)) ≤ (a + c + e) * (b + d + f) / (a + b + c + d + e + f)   :=  by sorry

Source

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

View graph