lean_workbook_plus_9293

Proved

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

Let $x,y,z\in\mathbb{R^+}$ .Prove that

\frac{x+2y}{z+2x+3y}+\frac{y+2z}{x+2y+3z}+\frac{z+2x}{y+2z+3x}>\frac{6}{7}.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_9293 (x y z : ℝ) (hx : 0 < x) (hy : 0 < y) (hz : 0 < z) : (x + 2 * y) / (z + 2 * x + 3 * y) + (y + 2 * z) / (x + 2 * y + 3 * z) + (z + 2 * x) / (y + 2 * z + 3 * x) > 6 / 7   :=  by sorry

Source

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

View graph