  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.
