Prove2Me

lean_workbook_plus_40024

Disproved

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

If (x,y)≠(1,1)(x,y)\ne (1,1), then (x+2y+1)2<(x+2y)2+2x+5y+9<(x+2y+2)2(x+2y+1)^2<(x+2y)^2+2x+5y+9<(x+2y+2)^2.

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_40024 : ∀ x y : ℝ, (x, y) ≠ (1, 1) → (x + 2 * y + 1) ^ 2 < (x + 2 * y) ^ 2 + 2 * x + 5 * y + 9 ∧ (x + 2 * y) ^ 2 + 2 * x + 5 * y + 9 < (x + 2 * y + 2) ^ 2   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph