lean_workbook_plus_15363

Disproved

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

Prove that $2-\frac{1}{2yz} \geq \frac{1}{y^2}+\frac{1}{z^2}-\frac{2}{yz}$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_15363 : ∀ y z : ℝ, (y * z ≠ 0 → 2 - 1 / (2 * y * z) ≥ 1 / y ^ 2 + 1 / z ^ 2 - 2 / (y * z))   :=  by sorry

Source