lean_workbook_plus_58588

Proved

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

Prove that, among any $13$ real numbers, there are two, $x$ and $y,$ such that $|x- y| \leq (2-\sqrt{2})|1+ xy|.$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_58588 (s : Finset ℝ) (hs : s.card ≥ 13) :
    ∃ x y, x ∈ s ∧ y ∈ s ∧ (abs (x - y) ≤ (2 - Real.sqrt 2) * abs (1 + x * y))   :=  by sorry

Source

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

View graph