Elementary Number Theory Problems. Part I

In this paper we demonstrate the feasibility of formalizing recreational mathematics in Mizar ([1], [2]) drawing examples from W. Sierpinski’s book “250 Problems in Elementary Number Theory” [4]. The current work contains proofs of initial ten problems from the chapter devoted to the divisibility of numbers. Included are problems on several levels of difficulty.Institute of Informatics, University of Białystok, PolandGrzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, Karol Pak, and Josef Urban. Mizar: State-of-the-art and beyond. In Manfred Kerber, Jacques Carette, Cezary Kaliszyk, Florian Rabe, and Volker Sorge, editors, Intelligent Computer Mathematics, volume 9150 of Lecture Notes in Computer Science, pages 261–279. Springer International Publishing, 2015. ISBN 978-3-319-20614-1. doi:10.1007/978-3-319-20615-8_17.Grzegorz Bancerek, Czesław Bylinski, Adam Grabowski, Artur Korniłowicz, Roman Matuszewski, Adam Naumowicz, and Karol Pak. The role of the Mizar Mathematical Library for interactive proof development in Mizar. Journal of Automated Reasoning, 61(1):9–32, 2018. doi:10.1007/s10817-017-9440-6.Marco Riccardi. The perfect number theorem and Wilson’s theorem. Formalized Mathematics, 17(2):123–128, 2009. doi:10.2478/v10037-009-0013-y.Wacław Sierpinski. 250 Problems in Elementary Number Theory. Elsevier, 1970.Tetsuya Tsunetou, Grzegorz Bancerek, and Yatsuka Nakamura. Zero-based finite sequences. Formalized Mathematics, 9(4):825–829, 2001.Li Yan, Xiquan Liang, and Junjie Zhao. Gauss lemma and law of quadratic reciprocity. Formalized Mathematics, 16(1):23–28, 2008. doi:10.2478/v10037-008-0004-4.11512