isabelle/valid/mathd_numbertheory_30.thy

(*
  Authors: Albert Qiaochu Jiang
*)

theory mathd_numbertheory_30 imports
Complex_Main

begin

theorem mathd_numbertheory_30:
  "(33818^2 + 33819^2 + 33820^2 + 33821^2 + 33822^2) mod 17 = (0::nat)"
  sorry


end