lean_workbook_plus_67158

Open

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

Prove that the product of the first $1000$ positive even integers differs from the product of the first $1000$ positive odd integers by a multiple of $2001$ .

Preamble

import Mathlib.Analysis.Complex.Basic

Formal statement

theorem lean_workbook_plus_67158 : (∏ i in Finset.range 1000, (2 * i + 2)) - (∏ i in Finset.range 1000, (2 * i + 1)) ≡ 0 [ZMOD 2001]   :=  by sorry

Source

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

View graph