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

(* Authors: Albert Qiaochu Jiang *) theory mathd_numbertheory_252 imports Complex_Main begin theorem mathd_numbertheory_252: "(fact 7) mod 23 = (3::nat)" sorry end