lean_workbook_plus_4240

Proved

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

Let $x,y,z>0$ such that $xyz=1$ . Prove that \n $\frac{x^{2}}{x^{2}+x+1}+\frac{y^{2}}{y^{2}+y+1}+\frac{z^{2}}{z^{2}+z+1}\geq 1$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_4240 (x y z : ℝ) (hx : x > 0) (hy : y > 0) (hz : z > 0) (habc : x * y * z = 1) : x^2 / (x^2 + x + 1) + y^2 / (y^2 + y + 1) + z^2 / (z^2 + z + 1) ≥ 1   :=  by sorry

Source

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

View graph