lean_workbook_plus_42072

Proved

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

Prove that for $x, y, z \geq 0$ and $x + y + z = 1$ , $\frac{1}{x^2 + 1} \leq \frac{54 - 27x}{50}$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_42072 (x y z : ℝ) (hx : x + y + z = 1) (hx' : 0 ≤ x) (hy' : 0 ≤ y) (hz' : 0 ≤ z) : 1 / (x ^ 2 + 1) ≤ (54 - 27 * x) / 50   :=  by sorry

Source

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

View graph