Prime Representing Polynomial with 10 Unknowns

Abstract

In this article we formalize in Mizar [1], [2] the final step of ourattempt to formally construct a prime representing polynomial with 10 variablesproposed by Yuri Matiyasevich in [4].The first part of the article includes many auxiliary lemmas related to multivariate polynomials. We start from the properties of monomials, among them their evaluation as well as the power function on polynomials to define the substitution for multivariate polynomials. For simplicity, we assume that a polynomialand substituted ones as i-th variable have the same number of variables. Then we study the number of variables that are used in given multivariate polynomials. By the used variable we mean a variable that is raised at least once to a non-zeropower. We consider both adding unused variables and eliminating them. The second part of the paper deals with the construction of the polynomialproposed by Yuri Matiyasevich. First, we introduce a diophantine polynomialover 4 variables that has roots in integers if and only if indicated variable is thesquare of a natural number, and another two is the square of an odd naturalnumber. We modify the polynomial by adding two variables in such a way thatthe root additionally requires the divisibility of these added variables. Then wemodify again the polynomial by adding two variables to also guarantee the nonnegativity condition of one of these variables. Finally, we combine the prime diophantine representation proved in [7] with the obtained polynomial constructinga prime representing polynomial with 10 variables. This work has been partiallypresented in [8] with the obtained polynomial constructing a prime representingpolynomial with 10 variables in Theorem (85).