lean_workbook_plus_65765

Proved

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

For $a, b, c>0$ prove that \n $\frac{4a+11b}{6a+13b+c}+\frac{4b+11c}{a+6b+13c}+\frac{4c+11a}{13a+b+6c}\leq\frac{9}{4}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_65765 (a b c : ℝ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) : (4*a + 11*b) / (6*a + 13*b + c) + (4*b + 11*c) / (a + 6*b + 13*c) + (4*c + 11*a) / (13*a + b + 6*c) ≤ 9 / 4   :=  by sorry

Source

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

View graph