Formalizing a Diophantine Representation of the Set of Prime Numbers

TL;DR

This paper formalizes the diophantine representation of prime numbers within the Mizar system, demonstrating the smallest known explicit polynomial with 10 variables and establishing the diophantine nature of exponential, factorial, and binomial functions.

Contribution

It provides the first formalization of the prime set representation in Mizar, using minimal variables and proving key functions are diophantine.

Findings

Prime numbers are represented with 10 variables in Mizar.

Exponential, factorial, and binomial functions are shown to be diophantine.

This formalization advances the understanding of diophantine sets and their representations.

Abstract

The DPRM (Davis-Putnam-Robinson-Matiyasevich) theorem is the main step in the negative resolution of Hilbert's 10th problem. Almost three decades of work on the problem have resulted in several equally surprising results. These include the existence of diophantine equations with a reduced number of variables, as well as the explicit construction of polynomials that represent specific sets, in particular the set of primes. In this work, we formalize these constructions in the Mizar system. We focus on the set of prime numbers and its explicit representation using 10 variables. It is the smallest representation known today. For this, we show that the exponential function is diophantine, together with the same properties for the binomial coefficient and factorial. This formalization is the next step in the research on formal approaches to diophantine sets following the DPRM theorem.