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

(* Authors: Albert Qiaochu Jiang *) theory mathd_numbertheory_101 imports Complex_Main begin theorem mathd_numbertheory_101: "(17 * 18) mod 4 = (2::nat)" by eval end