lean_workbook_plus_60962

Proved

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

Looking then at the equation mod $4$ , we get $2+x+y\equiv 3-xy\pmod 4$ and so $(x+1)(y+1)\equiv 2\pmod 4$ , impossible with $x,y$ both odd

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_60962  (x y : ℤ)
  (h₀ : Odd x ∧ Odd y)
  (h₁ : (x + 1) * (y + 1) ≡ 2 [ZMOD 4]) :
  False   :=  by sorry

Source