# Formalizing a Diophantine Representation of the Set of Prime Numbers

Source: [Formalizing a Diophantine Representation of the Set of Prime Numbers](<https://www.sota2.com/research/paper/68fa59311e209131ce9b4f4b>)

Collection index: [llms.txt](<https://www.sota2.com/research/llms.txt>)

Data updated: 2025-10-27T05:21:38.100Z

Authors: Karol P\\k{a}k, Cezary Kaliszyk

Published: 2022-04-26T13:41:05.000Z

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

## Recorded benchmark results

A research result applies to its stated dataset, split, metric and evaluation configuration. Compare like-for-like settings, preserve the metric's unit and direction, and distinguish paper-reported results from independent reproduction. The best result recorded here is not a claim of exhaustive, current global coverage.

## Original sources and implementation

[Original paper](<https://arxiv.org/abs/2204.12311>)

[PDF](<https://arxiv.org/pdf/2204.12311.pdf>)