Prime Representing Polynomial.

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, using the Mizar system [1], [2], in two independent ways, proving the existence of a polynomial without formulating it explicitly as well as with its indication. First, we reuse nearly all the techniques invented to prove the MRDP-theorem [11]. 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 [6] that has 26 variables in the Mizar language as follows (w center dot z+h+j-q)(2)+((g center dot k+g+k)center dot(h+j)+h-z)(2)+(2 center dot k(3)center dot(2 center dot k+2)center dot(n + 1)(2)+1-f(2))(2)+ (p + q + z + 2 center dot n - e)(2) + (e(3) center dot (e + 2) center dot (a + 1)(2) + 1 - o(2))(2) + (x(2) - (a(2) -' 1) center dot y(2) - 1)(2) + (16 center dot (a(2) - 1) center dot r(2) center dot y(2) center dot y(2) + 1 - u(2))(2) + (((a + u(2) center dot (u(2) - a))(2) - 1) center dot (n + 4 center dot d center dot y)(2) + 1 - (x + c center dot u)(2))(2) + (m(2) - (a(2) -' 1) center dot l(2) - 1)(2) + (k + i center dot (a - 1) - l)(2) + (n + l + v - y)(2) + (p + l center dot (a - n - 1) + b center dot (2 center dot a center dot (n + 1) - (n + 1)(2) - 1) - m)(2) + (q + y center dot (a - p - 1) + s center dot (2 center dot a center dot (p + 1) - (p + 1)(2) - 1) - x)(2) + (z + p center dot l center dot (a - p) + t center dot (2 center dot a center dot p - p(2) - 1) - p center dot m)(2) 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. 26 variables is not the best known result in relation to the set of prime numbers, since any diophantine equation over N can be reduced to one in 13 unknowns [8] or even less [5], [13]. The best currently known result for all prime numbers, where the polynomial is explicitly constructed is 10 [7] or even 7 in the case of Fermat as well as Mersenne prime number [4]. We are currently focusing our formalization efforts in this direction.