@ARTICLE{NUMBER15.MIZ,
  AUTHOR = {P\kak, Karol and Korni{\l}owicz, Artur},
  TITLE = {Elementary Number Theory Problems. {P}art {XV} -- Diophantine Equations},
  SECTION1 = {Preliminaries},
  SECTION2 = {Problem 38},
  SECTION3 = {Problem 58},
  SECTION4 = {Problem 160},
  SECTION5 = {Problem 164},
  SECTION6 = {Problem 168},
  SECTION7 = {Problem 171},
  SECTION8 = {Problem 188},
  SECTION9 = {Problem 195},
  SECTION10 = {Problem 196},
  SECTION11 = {Problem 198},
  DAY = {8},
  MONTH = {November},
  YEAR = {2024},
  ADDRESS1 = {Faculty of Computer Science\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  ADDRESS2 = {Faculty of Computer Science\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  MSC = {11A41 11D72 03B35 68V20},
  KEYWORDS = {number theory; prime number; Diophantine equation},
  SUMMARY = {This paper formalizes problems 38, 58, 160, 164, 168, 171, 188, 195, 196, and 198 from ``250 Problems in Elementary Number Theory'' by Wacław Sierpiński.},
  INTRODUCTION = {In this paper, Problems 38 from Section I, 58 from Section III, 160, 164, 168, 171, 188, 195, 196, and 198 
   from Section V of \cite{Sierpinski:1970} are formalized, using the Mizar formalism \cite{BancerekJAR:2018,Mizar-State-2015}. 
   The paper is a part of the project {\em Formalization of Elementary Number Theory in Mizar} \cite{Naumowicz:2020}.\par\bigskip\par
   In the preliminary section, we provided some valuable facts about the monotonicity of functions.\par\bigskip\par
   Problem 58 asks for a~proof that there exist arbitrarily long arithmetic progressions 
   formed of different positive integers, whose terms are powers of positive integers with integer exponents greater than 1.
   The proof in our formalization follows the evidence presented in the book with 
   a~small modification of numbering prime numbers (from 0, not from 1) caused by adequate operations stored in the MML. 
   Moreover, in the book it is written ``$p_k | a_n$ if $k \neq n$, where $n$ is a~positive integer $> s$'', 
   while $n$ must be $\leq s$ -- it is reflected in the definition of a~finite sequence {\tt sequenceAnPk(s,k)}.
   \par\bigskip\par
   Problem 160 requires finding all solutions in positive integers $x$, $y$, $z$, $t$, with $x \leq y \leq z \leq t$ of the equation
   $$\frac{1}{x} + \frac{1}{y} + \frac{1}{z} + \frac{1}{t} = 1.$$
   The proof given in the book presents 14 different solutions of the equation, but one of them
   $x = 2$,  $y = 4$,  $z = 5$, $t = 24$ is incorrect    
    $\left(\frac{1}{2} + \frac{1}{4} + \frac{1}{5} + \frac{1}{24} = \frac{119}{120} \neq 1\right)$.
   It should be $x = 2$,  $y = 4$,  $z = 5$, and $t = 20$. \par\bigskip\par
   Problem 168 concerns proving that for every positive integer $s$, the equation
   $$\frac{1}{x_1^2} + \frac{1}{x_2^2} + \cdots + \frac{1}{x_s^2} = \frac{1}{x_{s+1}^2}$$
   has infinitely many solutions in positive integers $x_1, x_2, \dots, x_s, x_{s+1}$.
   The original proof is splited into several cases -- but the case for $s = 2$ provides a~wrong 
   solution $\frac{1}{15^2} + \frac{1}{12^2} = \frac{1}{20^2}.$
   It should be $\frac{1}{15^2} + \frac{1}{20^2} = \frac{1}{12^2}.$\par\bigskip\par
   Problem 196 asks to solve the problem of A.~Moessner of finding all solutions in positive integers $x$, $y$, $z$, $t$ of the system of equations
   $$x+y = zt, z+t = xy$$
   where $x \leq y$ and $x \leq z \leq t$ 
   and to prove that this system has infinitely many integer solutions $x$, $y$, $z$, and $t$.
   The proof in the book is divided into several cases. The case for $x > 2$ is slightly imprecise.
   It claims that $z_1 t_1 + 2z_1 + 2t_1 + 4 \geq z_1 + t_1 + 9$, for $z_1 = z-2$, and $t_1 = t-2$, 
   but we could prove only inequality $z_1 t_1 + 2z_1 + 2t_1 + 4 \geq z_1 + t_1 + 7$.
   Anyway, our restriction could be used to complete the proof.\par\bigskip\par
   The proofs for the other problems are direct formalizations of the solutions presented in the book.}}
