isabelle/valid/mathd_numbertheory_198.thy (10 lines of code) (raw):

(* Authors: Albert Qiaochu Jiang *) theory mathd_numbertheory_198 imports Complex_Main begin theorem mathd_numbertheory_198: "(5^2005) mod 100 = (25::nat)" sorry end