lean_workbook_plus_34264

Proved

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

Take $n = (2k^2)^2 + (2k)^2$ then, \n $n = (2k^2)^2 + (2k)^2$ \n $n + 1 = (2k^2 + 1)^2 + 0^2$ \n $n + 2 = (2k^2 + 1)^2 + 1^2$

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_34264 (n k : ℕ) : n = (2 * k ^ 2) ^ 2 + (2 * k) ^ 2 → n + 1 = (2 * k ^ 2 + 1) ^ 2 + 0 ^ 2 ∧ n + 2 = (2 * k ^ 2 + 1) ^ 2 + 1 ^ 2   :=  by sorry

Source

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

View graph