@ARTICLE{HILB10_6.MIZ,
  AUTHOR = {P\k{a}k, Karol},
  TITLE = {Prime Representing Polynomial},
  SECTION1 = {The Prime Number Set as a Diophantine Set},
  SECTION2 = {Special Case of Pell's Equation - Selected Properties},
  SECTION3 = {Special Case of Pell's Equation - Diophantine Polynomial With 8 Variables},
  SECTION4 = {Prime Representing Polynomial with 26 Variables},
  DAY = {30},
  MONTH = {November},
  YEAR = {2021},
  ADDRESS1 = {Institute of Informatics\\University of Bia{\l}ystok\\ Konstantego Cio{\l}kowskiego 1M, 15-245 Bia{\l}ystok\\Poland},
  SUMMARY = {The main purpose of formalization is 
  to prove that the set of prime numbers is diophantine, 
  i.e., is representable by a polynomial formula.
We formalize this problem in two independent ways, 
proving the existence of a polynomial without 
formulating it explicitly as well as with its indication. 
\par
   First, we reuse nearly all the techniques invented
  to prove the MRDP-theorem \cite{HILB10_5.abs}.
  Applying a trick with Mizar schemes 
  that go beyond first-order logic
  we give a short sophisticated proof 
  for the existence of such a polynomial
  but without formulating it explicitly.
  Then we formulate the polynomial proposed in \cite{AMM76} that has 26 variables
  in the Mizar language as follows
  \begin{multline}
  [wz+h+j-q]^2+[(gk+g+k)(h+j)+h-z]^2+[(2k)^3(2k+2)(n+1)^2+1-f^2]^2 +\\
     [p+q+z+2n-e]^2+
     [e^3(e+2)(a+1)^2+1 -o^2]^2 +
     [x^2-(a^2-1)y^2-1]^2 +\\
     [16(a^2-1)r^2y^2y^2+1 -u^2)^2 +
     [((a+u^2(u^2-a))^2-1)(n+4dy)^2+1 -(x+cu)^2]^2 +\\
     [m^2-(a^2-1)l^2-1]^2 +
     [k+i(a-1)-l]^2 +
     [n+l+v-y]^2 +\\
     [p+l(a-n-1)+b(2a(n+1)-(n+1)^2-1)-m]^2+\\
     [q+y(a-p-1)+s(2a(p+1)-(p+1)^2-1)-x]^2+
     [z+pl(a-p)+t(2ap-p^2-1)-pm]^2\label{eq1}\end{multline}
  and we prove that 
  that for any positive integer $k$ so that
  $k+1$ is prime it is necessary and sufficient that
  there exist other natural variables $a$-$z$ for which
  the polynomial equals zero.}}

@ARTICLE{AMM76,
  AUTHOR =       {James P. Jones and Daihachiro Sato and Hideo Wada and  Douglas Wiens},
  TITLE =        {Diophantine Representation of the Set of Prime Numbers},
  JOURNAL =      {The American Mathematical Monthly},
  YEAR =         {1976},
  volume =       {83},
  number =       {6},
  pages =        {449-464}
}
