The main purpose of the article is to construct a sophisticated polynomial proposed by Matiyasevich and Robinson [5] that is often used to reduce the number of unknowns in diophantine representations, using the Mizar [1], [2] formalism. The polynomial
{J_k}\left( {{a_1}, \ldots ,{a_k},x} \right) = \prod\limits_{{\varepsilon _1}, \ldots ,{\varepsilon _k} \in \left\{ { \pm 1} \right\}} {\left( {x + {\varepsilon _1}\sqrt {{a_1}} + {\varepsilon _2}\sqrt {{a_2}} W} \right) + \ldots + {\varepsilon _k}\sqrt {{a_k}} {W^{k - 1}}}
with
W = \sum\nolimits_{i = 1}^k {x_i^2}
has integer coefficients and Jk(a1, . . ., ak, x) = 0 for some a1, . . ., ak, x ∈ ℤ if and only if a1, . . ., ak are all squares. However although it is nontrivial to observe that this expression is a polynomial, i.e., eliminating similar elements in the product of all combinations of signs we obtain an expression where every square root will occur with an even power. This work has been partially presented in [7].