Editing Hilbert's tenth problem (section)

==Further results==

We may speak of the ''degree'' of a Diophantine set as being the least degree of a polynomial in an equation defining that set. Similarly, we can call the ''dimension'' of such a set the fewest unknowns in a defining equation. Because of the existence of a universal Diophantine equation, it is clear that there are absolute upper bounds to both of these quantities, and there has been much interest in determining these bounds.

Already in the 1920s [[Thoralf Skolem]] showed that any Diophantine equation is equivalent to one of degree 4 or less. His trick was to introduce new unknowns by equations setting them equal to the square of an unknown or the product of two unknowns. Repetition of this process results in a system of second degree equations; then an equation of degree 4 is obtained by summing the squares. So every Diophantine set is trivially of degree 4 or less. It is not known whether this result is best possible.

Julia Robinson and Yuri Matiyasevich showed that every Diophantine set has dimension no greater than 13. Later, Matiyasevich sharpened their methods to show that 9 unknowns suffice. Although it may well be that this result is not the best possible, there has been no further progress.{{efn|At this point, even 3 cannot be excluded as an absolute upper bound.}} So, in particular, there is no algorithm for testing Diophantine equations with 9 or fewer unknowns for solvability in natural numbers. For the case of rational integer solutions (as Hilbert had originally posed it), the 4-squares trick shows that there is no algorithm for equations with no more than 36 unknowns. But [[Zhi Wei Sun]] showed that the problem for integers is unsolvable even for equations with no more than 11 unknowns.

Martin Davis studied algorithmic questions involving the number of solutions of a Diophantine equation. Hilbert's tenth problem asks whether or not that number is 0. Let <math>A=\{0,1,2,3,\ldots,\aleph_0\}</math> and let <math>C</math> be a proper non-empty subset of <math>A</math>. Davis proved that there is no algorithm to test a given Diophantine equation to determine whether the number of its solutions is a member of the set <math>C</math>. Thus there is no algorithm to determine whether the number of solutions of a Diophantine equation is finite, odd, a perfect square, a prime, etc.

The proof of the MRDP theorem has been formalized in [[Rocq (software)|Rocq]] (previously known as ''Coq'').<ref>{{cite report | url=http://www.ps.uni-saarland.de/Publications/documents/Larchey-WendlingForster_2019_H10_in_Coq.pdf | author=Dominique Larchey-Wendling and Yannick Forster | title=Hilbert's Tenth Problem in Coq | institution=[[Saarland University]] | type=Technical Report | year=2019 }} 
</ref>