lean_workbook_plus_47777

Disproved

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

Therefore, $2 \ge \left( {{x^2}{t^2} + xyzt + {y^2}{z^2}} \right) + \left( {{x^2}{z^2} + xyzt + {y^2}{t^2}} \right) \ge \dfrac{3}{4}{\left( {xt + yz} \right)^2} + \dfrac{3}{4}{\left( {xz + yt} \right)^2} \ge \dfrac{3}{8}{\left( {xt + yz + xz + yt} \right)^2} = \dfrac{3}{8}{\left( {x + y} \right)^2}{\left( {z + t} \right)^2}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_47777 :  ∀ x y z t : ℝ, 2 ≥ (x^2 * t^2 + x * y * z * t + y^2 * z^2) + (x^2 * z^2 + x * y * z * t + y^2 * t^2) ∧ (x^2 * t^2 + x * y * z * t + y^2 * z^2) + (x^2 * z^2 + x * y * z * t + y^2 * t^2) ≥ 3 / 4 * (x * t + y * z)^2 + 3 / 4 * (x * z + y * t)^2 ∧ 3 / 4 * (x * t + y * z)^2 + 3 / 4 * (x * z + y * t)^2 ≥ 3 / 8 * (x + y)^2 * (z + t)^2   :=  by sorry

Source

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

View graph