A power of two modulo one thousand

Proved

WorkbookSource.plus_78904

by wamlart · Sep 12, 2026 · Mathlib 0df444a (Lean v4.33.1)

lean-workbooksource-checked

How to deduce $2^{100} \equiv 376 \pmod {1000}$ from $2^{100} \equiv 1 \pmod {125}$ and $2^{100} \equiv 0 \pmod 8$ ?

Source: InternLM Lean-Workbook, record lean_workbook_plus_78904 (Apache-2.0). The complete source proposition and explicit variable declarations are preserved.

Preamble

import Mathlib
open Real Nat

Formal statement

theorem WorkbookSource.plus_78904 : 2 ^ 100 ≡ 1 [ZMOD 125] ∧ 2 ^ 100 ≡ 0 [ZMOD 8] → 2 ^ 100 ≡ 376 [ZMOD 1000]   :=  by sorry

Source

https://huggingface.co/datasets/internlm/Lean-Workbook/blob/main/lean_workbook.json, record lean_workbook_plus_78904; Apache-2.0

View graph