Worked solution: The MRDP theorem: Diophantine sets are exactly the recursively enumerable sets (1970)

Hilbert's tenth problem, the tenth of the twenty-three problems in his 1900 address to the International Congress of Mathematicians, asks for a procedure with finitely many operations that decides, for an arbitrary polynomial $P(x_1, \ldots, x_n) \in \mathbb{Z}[x_1, \ldots, x_n]$, whether the equation $P(x_1, \ldots, x_n) = 0$ is solvable in integers. Two features make the request strong: the algorithm must be uniform — one procedure covering all degrees and all coefficient tuples — and it must terminate with a correct yes/no answer on every input, not merely succeed on a decidable subclass.

Several subclasses were already decidable. Linear equations $a_1 x_1 + \cdots + a_n x_n = b$ reduce to computing $\gcd(a_1, \ldots, a_n)$; one-variable equations $P(x) = 0$ reduce, after clearing denominators, to divisibility of the constant term; and quadratic equations in two variables fall under the theory of binary quadratic forms and the Pell equation, essentially settled by continued fractions. What no classical technique could touch was the general case, where a Diophantine equation can encode arbitrarily intricate arithmetic structure and there is no bound on the number of unknowns $n$.

The resolution, completed by Matiyasevich in 1970, is negative, and it requires turning the informal word "procedure" into a mathematical object. The proof below follows the route surveyed in Matiyasevich's 2008 Scholarpedia article: identify Diophantine definability with recursive enumerability, then import Turing's undecidability of the halting problem.