lean_workbook_plus_27615

Proved

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

Let $S$ be the sum of the squares of the numbers on the board. Note that after each successive operation, $S$ always increases and never decreases since: $a^2+b^2 > 0 \implies 2a^2+2b^2 > a^2+b^2 \implies (a-b)^2+(a+b)^2 > a^2+b^2$ . Equality would hold if $a=b=0$ but that is impossible under the problem statement.

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_27615 :
  ∀ a b : ℤ, a ≠ 0 ∧ b ≠ 0 → (a - b) ^ 2 + (a + b) ^ 2 > a ^ 2 + b ^ 2   :=  by sorry

Source

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

View graph