Prove2Me

lean_workbook_plus_70834

Proved

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

Prove that 1x+y+z+t2+1x+y+z2+t+1x+y2+z+t+1x2+y+z+t≤14+t2−t+14−z+z2+14−y+y2+1x2+4−x\frac{1}{x+y+z+t^2}+\frac{1}{x+y+z^2+t}+\frac{1}{x+y^2+z+t}+\frac{1}{x^2+y+z+t}\le\frac{1}{4+t^2-t}+\frac{1}{4-z+z^2}+\frac{1}{4-y+y^2}+\frac{1}{x^2+4-x} given x,y,z,tx,y,z,t are positive numbers such that x+y+z+t≥4x+y+z+t\ge4.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_70834 (x y z t : ℝ) (h : x + y + z + t ≥ 4) : 1 / (x + y + z + t ^ 2) + 1 / (x + y + z ^ 2 + t) + 1 / (x + y ^ 2 + z + t) + 1 / (x ^ 2 + y + z + t) ≤ 1 / (4 + t ^ 2 - t) + 1 / (4 - z + z ^ 2) + 1 / (4 - y + y ^ 2) + 1 / (x ^ 2 + 4 - x)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph