Prove2Me

lean_workbook_plus_56504

Proved

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

Since 210≡1(mod11)2^{10}\equiv 1\pmod{11} from Fermat's Little Theorem, the remainder is 28=256≡3(mod11)2^8=256\equiv 3\pmod {11} .

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_56504 :
  (2^8) % 11 = 3   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph