lean_workbook_plus_64318

Proved

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

Setting $A=\sum\limits_{i=1}^{n}{t(k)}$ , $B=\sum\limits_{i=1}^{n}{s(k)}$ . We have $A+B=n(2n+1), A-B=\frac{n(n+3)}{2}$ This implies that $B+n=\frac{3n(n+1)}{4}$ . Since $B$ is an integer, it is obvious that $4|n(n+1)$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_64318  (n : ℕ)
  (h₀ : 0 < n)
  (h₁ : ∃ (A B : ℕ), A + B = n * (2 * n + 1) ∧ A - B = n * (n + 3) / 2) :
  4 ∣ n * (n + 1)   :=  by sorry

Source

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

View graph