LIPIcs.ITP.2019.33.pdf
- Filesize: 428 kB
- 7 pages
Document
The DPRM Theorem in Isabelle (Short Paper)
Authors
-
Part of:
Volume:
10th International Conference on Interactive Theorem Proving (ITP 2019)
Series: Leibniz International Proceedings in Informatics (LIPIcs)
Conference: International Conference on Interactive Theorem Proving (ITP) - License:
Creative Commons Attribution 3.0 Unported license
- Publication Date: 2019-09-05
File
Document Identifiers
Acknowledgements
We want to thank everyone who has contributed to this project: Deepak Aryal, Bogdan Ciurezu, Yiping Deng, Prabhat Devkota, Simon Dubischar, Malte Haßler, Yufei Liu and Maria Antonia Oprea. Without their involvement, most notably Yufei Liu’s implementation of is_diophantine, the project would not stand where it is today. Moreover, we would like to express our sincere gratitude to the entire welcoming and supportive Isabelle community. In particular, we are indebted to Mathias Fleury for all his help with Isabelle. Finally, a big thank you Yuri Matiyasevich for inspiring and initiating the project as well as to our supervisor Dierk Schleicher, for motivating us throughout the project, connecting us to many experts in the field, and all his critical feedback.
Cite AsGet BibTex
Jonas Bayer, Marco David, Abhik Pal, Benedikt Stock, and Dierk Schleicher. The DPRM Theorem in Isabelle (Short Paper). In 10th International Conference on Interactive Theorem Proving (ITP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 141, pp. 33:1-33:7, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ITP.2019.33
https://doi.org/10.4230/LIPIcs.ITP.2019.33
Abstract
Hilbert’s 10th problem asks for an algorithm to tell whether or not a given diophantine equation has a solution over the integers. The non-existence of such an algorithm was shown in 1970 by Yuri Matiyasevich. The key step is known as the DPRM theorem: every recursively enumerable set of natural numbers is Diophantine. We present the formalization of Matiyasevich’s proof of the DPRM theorem in Isabelle. To represent recursively enumerable sets in equations, we implement and arithmetize register machines. Using several number-theoretic lemmas, we prove that exponentiation has a diophantine representation. Further, we contribute a small library of number-theoretic implementations of binary digit-wise relations. Finally, we discuss and contribute an is_diophantine predicate. We expect the complete formalization of the DPRM theorem in the near future; at present it is complete except for a minor gap in the arithmetization proofs of register machines and extending the is_diophantine predicate by two binary digit-wise relations.
Subject Classification
ACM Subject Classification
- Theory of computation → Automated reasoning
- Theory of computation → Higher order logic
Keywords
- DPRM theorem
- Hilbert’s tenth problem
- Diophantine predicates
- Register machines
- Recursively enumerable sets
- Isabelle
- Formal verification
Metrics
- Access Statistics
-
Total Accesses (updated on a weekly basis)
0PDF Downloads
References
-
Jonas Bayer, Marco David, Abhik Pal, and Benedikt Stock. Beginners' Quest to Formalize Mathematics: A Feasibility Study in Isabelle. In C. Kaliszyk, E. Brady, A. Kohlhase, and C. Sacerdoti Coen, editors, Conference on Intelligent Computer Mathematics., volume 11617 of Lecture Notes in Computer Science, 2019. (to appear).
- Mario Carneiro. A Lean formalization of Matiyasevič’s Theorem. URL: http://arxiv.org/abs/1802.01795v1.
- Yannick Forster Dominique Larchey-Wendling. Hilbert’s Tenth Problem in Coq. URL: http://www.ps.uni-saarland.de/Publications/documents/Larchey-WendlingForster_2019_H10_in_Coq.pdf.
-
Yuri Matiyasevich. On Hilbert’s Tenth Problem. In Michael Lamoureux, editor, PIMS Distinguished Chair Lectures, volume 1. Pacific Institute for the Mathematical Sciences, 2000.
- Karol Pąk. Progress in the Formalization of Matiyasevich’s theorem in the Mizar system. URL: http://alioth.uwb.edu.pl/~pakkarol/articles/FMM_2018_KP.pdf.
-
Jian Xu, Xingyuan Zhang, and Christian Urban. Mechanising Turing Machines and Computability Theory in Isabelle/HOL. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Interactive Theorem Proving. ITP 2013., volume 7998 of Lecture Notes in Computer Science, pages 147-162. Springer Berlin, Heidelberg, 2013.