Prove2Me

lean_workbook_plus_38916

Disproved

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

25k≡1(mod5)2^{5k}\equiv1\pmod5 \n 25k+1≡2(mod5)2^{5k+1}\equiv2\pmod5 \n 25k+2≡4(mod5)2^{5k+2}\equiv4\pmod5 \n 25k+3≡3(mod5)2^{5k+3}\equiv3\pmod5 \n 25k+4≡1(mod5)2^{5k+4}\equiv1\pmod5 \n \n 35k≡1(mod5)3^{5k}\equiv1\pmod5 \n 35k+1≡3(mod5)3^{5k+1}\equiv3\pmod5 \n 35k+2≡4(mod5)3^{5k+2}\equiv4\pmod5 \n 35k+3≡2(mod5)3^{5k+3}\equiv2\pmod5 \n 35k+4≡1(mod5)3^{5k+4}\equiv1\pmod5

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_38916 : ∀ k : ℕ, (2 ^ (5 * k) ≡ 1 [ZMOD 5]) ∧ (2 ^ (5 * k + 1) ≡ 2 [ZMOD 5]) ∧ (2 ^ (5 * k + 2) ≡ 4 [ZMOD 5]) ∧ (2 ^ (5 * k + 3) ≡ 3 [ZMOD 5]) ∧ (2 ^ (5 * k + 4) ≡ 1 [ZMOD 5])   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph