LIPIcs.ITP.2022.26.pdf
- Filesize: 0.71 MB
- 8 pages
Document
Formalizing a Diophantine Representation of the Set of Prime Numbers
Authors
Karol Pąk 
,
Cezary Kaliszyk
-
Part of:
Volume:
13th International Conference on Interactive Theorem Proving (ITP 2022)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 4.0 International license
- Publication Date: 2022-08-03
File
Document Identifiers
Author Details
Acknowledgements
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)
https://doi.org/10.4230/LIPIcs.ITP.2022.26
https://doi.org/10.4230/LIPIcs.ITP.2022.26
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.
Subject Classification
ACM Subject Classification
- Theory of computation → Interactive proof systems
Keywords
- DPRM theorem
- Polynomial reduction
- prime numbers
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
- 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: https://doi.org/10.4230/LIPIcs.ITP.2019.33.
- Mario Carneiro. A Lean formalization of Matiyasevič’s theorem, 2018. URL: http://arxiv.org/abs/1802.01795.
- Martin Davis. Arithmetical problems and recursively enumerable predicates. J. Symb. Log., 18(1):33-41, 1953. URL: https://doi.org/10.2307/2266325.
- Martin Davis, Hilary Putnam, and Julia Robinson. The decision problem for exponential diophantine equations. Annals of Mathematics, 74:425-436, 1961. URL: https://doi.org/10.2307/1970289.
-
James P. Jones. Universal diophantine equation. The Journal of Symbolic Logic, 45(3):549-571, 1982.
-
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.
-
Michael Lamoureux, editor. On Hilbert’s Tenth Problem, volume 1. Pacific Institute for the Mathematical Sciences, PIMS Distinguished Chair Lectures, 2000.
- 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: https://doi.org/10.4230/LIPIcs.FSCD.2019.27.
-
Yuri Matiyasevich. Enumerable sets are diophantine. Doklady Akademii Nauk SSSR (in Russian), 191:279-282, 1970.
- Yuri Matiyasevich. Primes are nonnegative values of a polynomial in 10 variables. Journal of Soviet Mathematics, 15:33-44, 1981. URL: https://doi.org/10.1007/BF01404106.
-
Yuri Matiyasevich and Julia Robinson. Reduction of an arbitrary diophantine equation to one in 13 unknowns. Acta Arithmetica, 27:521-553, 1975.
- Karol Pąk. Formalization of the MRDP theorem in the Mizar system. Formalized Mathematics, 27(2):209-221, 2019. URL: https://doi.org/10.2478/forma-2019-0020.
- Karol Pąk. Formalization of prime representing polynomial in Mizar. In FMM 2021 workshop, 2021. URL: http://alioth.uwb.edu.pl/~pakkarol/articles/KP-FMM2021.pdf.
- Karol Pąk. The Matiyasevich Theorem. Preliminaries. Formalized Mathematics, 25(4):315-325, 2017. URL: https://doi.org/10.1515/forma-2017-0029.
-
Julia Robinson. Diophantine decision problems. Studies in number theory, 6:76-116, 1969.
-
Craig Alan Smorynski. Logical Number Theory I, An Introduction. Universitext. Springer-Verlag Berlin Heidelberg, 1991.
- Zhi-Wei Sun. Further results on Hilbert’s Tenth Problem. Science China Mathematics, 64:281-306, 2021. URL: https://doi.org/10.1007/s11425-020-1813-5.