Prove2Me

lean_workbook_plus_75332

Disproved

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

Let xx be real number . Prove that \n

x2+(1x−1)2+1(x−1)2≥5x^2+(\frac{1}{x}-1)^2+\frac{1}{(x-1)^2}\geq 5 x2+(4x−1)2+1(x−1)2≥6x^2+(\frac{4}{x}-1)^2+\frac{1}{(x-1)^2} \geq 6 x2+(1x−1)2+(1x+1)2≥2(2+1)x^2+(\frac{1}{x}-1)^2+(\frac{1}{x}+1)^ 2\geq 2(\sqrt 2+1)
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_75332 : ∀ x : ℝ, x^2 + (1/x - 1)^2 + 1/(x-1)^2 ≥ 5 ∧ x^2 + (4/x - 1)^2 + 1/(x-1)^2 ≥ 6 ∧ x^2 + (1/x - 1)^2 + (1/x + 1)^2 ≥ 2 * (Real.sqrt 2 + 1)   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph