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 𝑐 𝑖 𝑣 1 𝑣 2 𝑣 3 . . . 𝑣 𝑗 where the coefficients 𝑐 𝑖 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 sufficient that there exist other natural variables 𝑎-𝑧 for which the polynomial

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:31 for f,k be positive Nat holds f = k! iff ex j,h,n,p,q,w,z be positive Nat st

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).

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].