The aim of our work is to show, using the Mizar system that our techniques invented to formalize the unsolvability of Hilbert's tenth problem in a Matiyasevich way, can be reused to prove that an assumption used by Julia Robinson demonstrates the same result independently. We present our formalization that the set of prime numbers is representable by a polynomial formula. Martin Davis, YuriMatiyasevich, Hilary Putnam and Julia Robinson [DPR61, Mat70] have proven that every recursively enumerable set is diophantine, and hence prove the Hilbert's Tenth Problem in the negative: there is no algorithmic way of determining whether some arbitrary diophantine equation has a solution. This is known as the MRDP-theorem (due to Matiyasevich, Robinson, Davis, and Putnam). This problem took seventy years to resolve, during which many attempts have been made to solve the problem. It is therefore not surprising that Julia Robinson and Martin Davis, with a contribution from Hilary Putnam, created several theorems that give a negative solution to the problem but under some assumptions. One of these assumptions that the exponential function can be defined in a diophantine way has been eliminated by Yuri Matiyasevich using a trick with clever use of Fibonacci numbers, who definitively completed the proof of the MRDP-theorem. In our work, we focus on another theorem under some, currently eliminated assumption, proposed by Julia Robinson [Rob69]. She proved that if the set of prime numbers was diophantine, then every recursively enumerable set would be diophantine. We do this for two main reasons. First, the set of prime numbers can be representable by a complicated polynomial formula (proposed in [JSWW76]) and consequently, the set is diophantine. We can investigate the possibilities of the Mizar system [? GKN15] to prove that explicitly given polynomial with 26 variables determine the set of prime numbers. We also use a trick with Mizar schemes (see [GKN10]) that go beyond first-order logic to show a sophisticated proof of the existence of such a polynomial without formulating it explicitly. Second, the proof of the assumption requires
nearly all the techniques invented to prove the MRDP-theorem that we formalized in the Mizar system [Pąk19b] and seems a natural continuation of the formal approach to diophantine sets.
Obviously, we need to begin by quickly explaining what we mean by diophantine. A diophantine polynomial in the variables 1, 2, . . . , is defined in informal mathematical practice as finite sum of expressions of the type 123 . . . where the coeficients are integers (positive or negative) and are variables. A diophantine equation, in traditional form is an equation of the form (1, . . . , , 1, . . . , ) = 0, where is a diophantine polynomial, 1, . . . , , 1, ..., indicate parameters and unknowns, respectively. A set ⊆ N of -tuples is called diophantine if there exists a + –variable diophantine polynomial such that ⟨1, . . . , ⟩ ∈ if and only if there exist variables 1, . . . , ∈ N such that (1, . . . , , 1, . . . , ) = 0.
In the context of the MRDP-theorem, we repeatedly refer to concepts of diophantine polynomials, equations, and sets, but in a slightly inverted way. Instead of being given an equation and seeking its solutions, we will give a set of solutions and seek a corresponding diophantine equation. In particular, the set of numbers which are either even or multiples of three is diophantine, since ( − 2)( − 3) takes a zero for each , which is either even or a multiple of three. Similarly, the set of numbers which are even and multiples of three is diophantine, since ( − 2)2 + ( − 3)2 or simply − 6 takes a zero for such . It is easy to see that in the general case a diophantine polynomial is not determined uniquely by a given diophantine set. So we might ask what is the smallest possible degree and/or what is the smallest possible number of parameters in a diophantine polynomial to determine a given diophantine set. In our simple example the question is straightforward, but it is not so for the set of prime numbers. In 1971, Yuri Matiyasevich give the construction of a diophantine polynomial with 24 variables and degree 37 that determines the set of prime numbers. Using the Skolem substitution method [Dav73] we can reduce the degree to 5. However, this procedure increases the number of variables. Currently, the smallest known number of variables to represent primes is 12 and is proposed by Yuri Matiyasevich and Julia Robinson in [MR75], but the degree of the polynomial is more than a few thousand (more than 6,000 from our estimate).
In our Mizar formalization, we chose a diophantine polynomial with 26 variables to represent primes that is given in [JSWW76]. We show that for any positive integer so that + 1 is prime it is necessary and suficient that there exist other natural variables - for which the polynomial [ + ℎ + − ]2 + [( + + )(ℎ + ) + ℎ − ]2 + [(2)3(2 + 2)( + 1)2 + 1 − 2]2+ [ + + + 2 − ]2 + [3( + 2)( + 1)2 + 1 − 2]2 + [2 − (2 − 1)2 − 1]2+ [16(2 − 1)222 + 1 − 2)2 + [(( + 2(2 − ))2 − 1)( + 4)2 + 1 − ( + )2]2+ [2 − (2 − 1)2 − 1]2 + [ + ( − 1) − ]2 + [ + + − ]2+
[ + ( − − 1) + (2( + 1) − ( + 1)2 − 1) − ]2+ [ + ( − − 1) + (2( + 1) − ( + 1)2 − 1) − ]2 + [ + ( − ) + (2 − 2 − 1) − ]2 equals zero.
The proof that (1) determine the set of prime numbers is based on two concepts: the special case of Pell’s Equation that has the form 2 − (2 − 1)2 = 1, where > 1 and Wilson’s theorem which characterizes the primes in terms of the factorial function, i.e., for any positive integers holds + 1 is prime if and only if + 1|! + 1. Note that we had to prove that the equality = ! is diophantine since it is one of the key steps to proving the MRDP-theorem and the theorem is already formulated in [Pąk19a] as follows: theorem :: HILB10_4:31 for i1,i2 be Element of n st n<>0 holds
{p where p is n-element XFinSequence of NAT: p.i1 = p.i2!} is diophantine Subset of n-xtuples_of NAT; Note that i be Element of n means in particular that i is in the domain of a zero-based indices, ntuples p, since n={0,1,2,. . .,n-1} in the standard construction of the natural numbers developed in the Mizar library. Rather than showing full proof that the set of prime numbers is diophantine, we just show a trick with Mizar schemes (second-order theorems) that provide the ability to combine diophantine relation using conjunctions and alternatives as well as a special case to substitution (see [AP18]): scheme :: HILB10_3:sch 4 Substitution{P[Nat,Nat,natural object,Nat,Nat,Nat], F(Nat,Nat,Nat)→natural object}: for i1,i2,i3,i4,i5 holds {p: P[p.i1,p.i2,F(p.i3,p.i4,p.i5),p.i3,p.i4,p.i5]}
is diophantine Subset of n-xtuples_of NAT provided for i1,i2,i3,i4,i5,i6 holds {p: P[p.i1,p.i2,p.i3,p.i4,p.i5,p.i6]}
is diophantine Subset of n-xtuples_of NAT and for i1,i2,i3,i4 holds {p: F(p.i1,p.i2,p.i3) = p.i4}
is diophantine Subset of n-xtuples_of NAT; Since the truncated subtraction (diference or zero) represented in Mizar as -′ is diophantine theorem :: HILB10_3:20 for a,b,c be Integer, i1,i2,i3 be Element of n holds
{p where p is n-element XFinSequence of NAT: a∗p.i1 = b∗p.i2-′c} is diophantine Subset of n -xtuples_of NAT; we conclude in particular that {p: p.i1 = p.i2-′1} is also diophantine. Combining these with HILB10_4:31 and using Substitution we obtain that {p: p.i1 = (p.i2-′1)!} is diophantine. This is proved by writing = 1 2 3. 2 -′ 1, = 1 2 3 4 5 6. 4 = 3!. Note that most of the arguments of , are unused. We have decided on such a solution in order to avoid repeating the substitution schemes for individual cases of arity, since such arity of , was suficient to apply all substitutions done in the MRDP-theorem. In the same manner we can see that {p: p.i1 = (p. i2-′1)! + 1} is diophantine writing = 1 2 3. (2 -′ 1)!, = 1 2 3 4 5 6. 4 = 1∗3+1 and using the following theorem: theorem :: HILB10_3:15 for a,b be Integer, i1,i2 be Element of n holds
{p where p is n-element XFinSequence of NAT: p.i1 = a∗p.i2+b} is diophantine Subset of n-xtuples_of NAT; Next, using again the Substitution with the fact that the congruence is diophantine and writing = 1 2 3. (2 -′ 1)!+1, = 1 2 3 4 5 6. 1∗3, 0∗4 are_congruent_mod 1∗4, we obtain that {p: (p.i-′1)! + 1 mod p.i = 0} is diophantine. theorem :: HILB10_3:3 for a,b,c be Integer, i1,i2,i3 be Element of n holds {p where p is n-element XFinSequence of NAT:
a∗p.i1,b∗p.i2 are_congruent_mod c∗p.i3} is diophantine Subset of n-xtuples_of NAT; We continue in this fashion with HILB10_3:7 and obtain that {p: p.i > 0} is diophantine. theorem :: HILB10_3:7 for a,b,c be Integer, i1,i2 be Element of n holds
{p where p is n-element XFinSequence of NAT: a∗p.i1 > b∗p.i2+c} is diophantine Subset of n-xtuples_of NAT; scheme :: HILB10_3:sch 3 IntersectionDiophantine{n()→Nat,P,Q[XFinSequence]}: {p where p is n()-element XFinSequence of NAT: P[p] & Q[p]}
is diophantine Subset of n()-xtuples_of NAT provided {p where p is n()-element XFinSequence of NAT: P[p]}
is diophantine Subset of n()-xtuples_of NAT and {p where p is n()-element XFinSequence of NAT: Q[p]}
is diophantine Subset of n()-xtuples_of NAT; Finally, using the IntersectionDiophantine scheme we can conclude that the intersection of these sets, that is equal to {p: (p.i-′1)! + 1 mod p.i = 0 & p.i > 1} is diophantine. Then the proof that the set of prime numbers is diophantine is easy to complete by applying the Wilson’s theorem [Pąk21]. theorem :: HILB10_6:4 for i being Element of n holds
{p where p is n-element XFinSequence of NAT: p.i is prime} is diophantine Subset of n-xtuples_of NAT Using such techniques invented to prove the MRDP-theorem in [Pąk19b] we needed less than 100 lines of code to complete the, but the prime representing polynomial is deeply hidden in the proof, e.g., in the constructions used in the schemes. Moreover, we need a more sophisticated list of arithmetical properties than the one used in [Pąk19a] to to reduce the number of variables to 26 which occur in (1).
For this purpose, we formalize additional properties of the special case of Pell’s Equation by following the idea presented in [JSWW76] as follows: theorem :: HILB10_6:24 for a be non trivial Nat for y,n be Nat st 1 <= n holds y = Py(a,n) if ex c,d,r,u,x be Nat st [x,y] is Pell s_solution of a^2-′1 & u^2 = 16∗(a^2-1)∗r^2∗y^2∗y^2+1 & (x+c∗u)^2 = ((a+u^2∗(u^2-a))^2-1)∗(n+4∗d∗y)^2+1 & n <= y; theorem :: HILB10_6:31 for f,k be positive Nat holds f = k! if ex j,h,n,p,q,w,z be positive Nat st q = w∗z+h+j & z = f∗(h+j)+h & (2∗k)|^3∗(2∗k+2)∗(n+1)|^2+1 is square & p = (n+1)|^k & q = (p+1)|^n & z = p|^(k+1); where the truncated subtraction, the second power, the nth power are represented as -′, ^2, |^n, respectively. Now we are ready to express and prove in the Mizar system that the set of prime numbers is representable by the polynomial formula (1). theorem :: HILB10_6:33 for k be positive Nat holds k+1 is prime if ex a,b,c,d,e,f,g,h,i,j,l,m,n,o,p,q,r,s,t,u,w,v,x,y,z be Nat st 0 = (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;
Our formalization has so far focused on the polynomial proposed in [JSWW76]. We showed formally in the Mizar system that the polynomial determines the set of prime numbers, hence the set is diophantine. Now we are working on reducing the number of variables in the considered polynomial to 12 as has been done by Yuri Matiyasevich and Julia Robinson in [MR75].