Prime Representing Polynomial
Karol Pąk · Formalized Mathematics · 2021
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, 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 · z + h + j − q ) 2 +(( g · k + g + k )·( h + j )+ h − z ) 2 +(2 · k 3 ·(2· k +2)·( n + 1) 2 +1− f 2 ) 2 + ( p + q + z + 2 · n − 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 2 · y 2 · y 2 + 1 − u 2 ) 2 + ((( a + u 2 · ( u 2 − a )) 2 − 1) · ( n + 4 · d · y ) 2 + 1 − ( x + c · u ) 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 · (2 · a · ( n + 1) − ( n + 1) 2 − 1) − m ) 2 + ( q + y · ( a − p − 1) + s · (2 · a · ( p + 1) − ( p + 1) 2 − 1) − x ) 2 + ( z + p · l · ( a − p ) + t · (2 · a · p − p 2 − 1) − p · 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 ℕ 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 th