Prove2Me

lean_workbook_plus_7188

Disproved

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

Just write 2(x2−1)(y2−1)≤1−x2+1−y2≤2(x−1)(y−1)+12\sqrt{(x^{2}-1)(y^{2}-1)}\leq{1-x^{2}+1-y^{2}}\leq{2(x-1)(y-1)+1} .Last inequality is from obvious (x+y−1)2≥0(x+y-1)^{2}\geq{0}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_7188 :
  ∀ x y : ℝ,
    2 * Real.sqrt ((x^2 - 1) * (y^2 - 1)) ≤ 1 - x^2 + 1 - y^2 ∧
    1 - x^2 + 1 - y^2 ≤ 2 * (x - 1) * (y - 1) + 1   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph