The DPRM (Davis-Putnam-Robinson-Matiyasevich) theorem is the main step in the negative resolution of Hilbert's 10th problem. Almost three decades of work on the problem have resulted in several equally surprising results. These include the existence of diophantine equations with a reduced number of variables, as well as the explicit construction of polynomials that represent specific sets, in particular the set of primes. In this work, we formalize these constructions in the Mizar system. We focus on the set of prime numbers and its explicit representation using 10 variables. It is the smallest representation known today. For this, we show that the exponential function is diophantine, together with the same properties for the binomial coefficient and factorial. This formalization is the next step in the research on formal approaches to diophantine sets following the DPRM theorem.

翻译：DPRM (Davis- Putnam- Robinson-Matiyasevich) 理论是否定解决Hilbert第10个问题的主要步骤。 近30年有关该问题的工作已经产生了若干同样令人惊讶的结果, 其中包括存在二异方程式, 变量数量减少, 以及明确构建代表特定组数, 特别是质数组数的多异方程式。 在这项工作中, 我们将这些构造正式化在 Mizar 系统中。 我们用10个变量来关注质数组及其明确的表达方式。 这是今天已知最小的表示方式 。 对此, 我们显示指数函数是二异体元素, 以及二异体系数和因子系数的相同特性 。 这个正规化是研究二异体定型方法的下一个步骤 。