isabelle/valid/mathd_numbertheory_269.thy (10 lines of code) (raw):
(*
Authors: Albert Qiaochu Jiang
*)
theory mathd_numbertheory_269 imports
Complex_Main
begin
theorem mathd_numbertheory_269:
"(2005^2 + 2005^0 + 2005^0 + 2005^5) mod 100 = (52::nat)"
sorry
end