### 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

BSD License

### Topics

- Logic/Computability
- Mathematics/Number theory

### 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

### Depends on

- Digit Expansions
- Lucas’s Theorem

### Auto-related entries

- p-adic Fields and p-adic Semialgebraic Sets

## Cite

×

DPRM_Theorem-AFP

    @article{DPRM_Theorem-AFP,
      author  = {Jonas Bayer and Marco David and Benedikt Stock and Abhik Pal and Yuri Matiyasevich and Dierk Schleicher},
      title   = {Diophantine Equations and the DPRM Theorem},
      journal = {Archive of Formal Proofs},
      month   = {June},
      year    = {2022},
      note    = {\url{https://isa-afp.org/entries/DPRM_Theorem.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Jun 7, 2022 : Isabelle2021-1