lean_workbook_plus_1266

Disproved

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

prove that \n $\frac{x^2}{x^2+y^2+yz}+\frac{y^2}{y^2+z^2+xz}+\frac{z^2}{z^2+x^2+xy}\geq1.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_1266 : ∀ x y z : ℝ, (x ^ 2 / (x ^ 2 + y ^ 2 + y * z) + y ^ 2 / (y ^ 2 + z ^ 2 + z * x) + z ^ 2 / (z ^ 2 + x ^ 2 + x * y) ≥ 1)   :=  by sorry

Source

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

View graph