Prove2Me

lean_workbook_plus_18679

Proved

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

A(mod3)≡22010+52011(mod3)≡22010+5⋅52010(mod3)≡(−1)2010+−1⋅(−1)2010(mod3)≡1−1(mod3)≡0(mod3)A \pmod{3} \equiv 2^{2010}+5^{2011} \pmod{3} \equiv 2^{2010}+5 \cdot 5^{2010} \pmod{3} \equiv \left(-1\right)^{2010}+-1 \cdot \left(-1\right)^{2010} \pmod{3} \equiv 1-1 \pmod{3} \equiv \boxed{0} \pmod{3}

Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_18679 :
  (2^2010 + 5^2011) % 3 = 0   :=  by sorry
Source
https://huggingface.co/datasets/internlm/Lean-Workbook

View graph