Prove2Me

lean_workbook_plus_42372

Proved

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

Given 2=x2+y2+z2≥x2+y2≥2xy2 = x^2 + y^2 + z^2 \geq x^2 + y^2 \geq 2xy, prove that 1−xy≥01 - xy \geq 0, 1−xz≥01 - xz \geq 0, and 1−yz≥01 - yz \geq 0.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_42372 (x y z : ℝ) (h₁ : 2 = x^2 + y^2 + z^2) (h₂ : x^2 + y^2 ≥ 2 * x * y) : 1 - x * y ≥ 0 ∧ 1 - x * z ≥ 0 ∧ 1 - y * z ≥ 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph