Formalizing a Diophantine Representation of the Set of Prime Numbers

Authors Karol Pąk , Cezary Kaliszyk

Thumbnail PDF


  • Filesize: 0.71 MB
  • 8 pages

Document Identifiers

Author Details

Karol Pąk
  • University of Białystok, Poland
Cezary Kaliszyk
  • Universität Innsbruck, Austria


We would like to thank Yuri Matiyasevich for his comments on the previous version of this paper.

Cite AsGet BibTex

Karol Pąk and Cezary Kaliszyk. Formalizing a Diophantine Representation of the Set of Prime Numbers. In 13th International Conference on Interactive Theorem Proving (ITP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 237, pp. 26:1-26:8, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Interactive proof systems
  • DPRM theorem
  • Polynomial reduction
  • prime numbers


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads


  1. Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher. The DPRM theorem in Isabelle (short paper). In John Harrison, John O'Leary, and Andrew Tolmach, editors, 10th International Conference on Interactive Theorem Proving, ITP 2019, volume 141 of LIPIcs, pages 33:1-33:7. Dagstuhl, 2019. URL:
  2. Mario Carneiro. A Lean formalization of Matiyasevič’s theorem, 2018. URL:
  3. Martin Davis. Arithmetical problems and recursively enumerable predicates. J. Symb. Log., 18(1):33-41, 1953. URL:
  4. Martin Davis, Hilary Putnam, and Julia Robinson. The decision problem for exponential diophantine equations. Annals of Mathematics, 74:425-436, 1961. URL:
  5. James P. Jones. Universal diophantine equation. The Journal of Symbolic Logic, 45(3):549-571, 1982. Google Scholar
  6. James P. Jones, Daihachiro Sato, Hideo Wada, and Douglas Wiens. Diophantine representation of the set of prime numbers. The American Mathematical Monthly, 83(6):449-464, 1976. Google Scholar
  7. Michael Lamoureux, editor. On Hilbert’s Tenth Problem, volume 1. Pacific Institute for the Mathematical Sciences, PIMS Distinguished Chair Lectures, 2000. Google Scholar
  8. Dominique Larchey-Wendling and Yannick Forster. Hilbert’s Tenth Problem in Coq. In Herman Geuvers, editor, 4th International Conference on Formal Structures for Computation and Deduction (FSCD 2019), volume 131 of LIPIcs, pages 27:1-27:20, Dagstuhl, Germany, 2019. Dagstuhl. URL:
  9. Yuri Matiyasevich. Enumerable sets are diophantine. Doklady Akademii Nauk SSSR (in Russian), 191:279-282, 1970. Google Scholar
  10. Yuri Matiyasevich. Primes are nonnegative values of a polynomial in 10 variables. Journal of Soviet Mathematics, 15:33-44, 1981. URL:
  11. Yuri Matiyasevich and Julia Robinson. Reduction of an arbitrary diophantine equation to one in 13 unknowns. Acta Arithmetica, 27:521-553, 1975. Google Scholar
  12. Karol Pąk. Formalization of the MRDP theorem in the Mizar system. Formalized Mathematics, 27(2):209-221, 2019. URL:
  13. Karol Pąk. Formalization of prime representing polynomial in Mizar. In FMM 2021 workshop, 2021. URL:
  14. Karol Pąk. The Matiyasevich Theorem. Preliminaries. Formalized Mathematics, 25(4):315-325, 2017. URL:
  15. Julia Robinson. Diophantine decision problems. Studies in number theory, 6:76-116, 1969. Google Scholar
  16. Craig Alan Smorynski. Logical Number Theory I, An Introduction. Universitext. Springer-Verlag Berlin Heidelberg, 1991. Google Scholar
  17. Zhi-Wei Sun. Further results on Hilbert’s Tenth Problem. Science China Mathematics, 64:281-306, 2021. URL: