### Abstract

We present a formalization of Matiyasevich's proof of the DPRM
theorem, which states that every recursively enumerable set of natural
numbers is Diophantine. This result from 1970 yields a negative
solution to Hilbert's 10th problem over the integers. To
represent recursively enumerable sets in equations, we implement and
arithmetize register machines. We formalize a general theory of
Diophantine sets and relations to reason about them abstractly. Using
several number-theoretic lemmas, we prove that exponentiation has a
Diophantine representation.

### License

### Topics

### Session DPRM_Theorem

- Parametric_Polynomials
- Assignments
- Diophantine_Relations
- Existential_Quantifier
- Modulo_Divisibility
- Exponentiation
- Alpha_Sequence
- Exponential_Relation
- Digit_Function
- Binomial_Coefficient
- Binary_Orthogonal
- Binary_Masking
- Binary_And
- RegisterMachineSpecification
- RegisterMachineProperties
- RegisterMachineSimulation
- SingleStepRegister
- SingleStepState
- MultipleStepRegister
- MultipleStepState
- MachineMasking
- MachineEquations
- CommutationRelations
- MultipleToSingleSteps
- Equation_Setup
- Register_Machine_Sums
- RM_Sums_Diophantine
- Register_Equations
- State_0_Equation
- State_d_Equation
- State_Unique_Equations
- All_State_Equations
- Mask_Equations
- Constants_Equations
- All_Equations_Invariance
- All_Equations
- Machine_Equation_Equivalence
- DPRM