A Lean formalization of Matiyasevi\v{c}'s Theorem
Logic
2018-02-07 v1
Abstract
In this paper, we present a formalization of Matiyasevi\v{c}'s theorem, which states that the power function is Diophantine, forming the last and hardest piece of the MRDP theorem of the unsolvability of Hilbert's 10th problem. The formalization is performed within the Lean theorem prover, and necessitated the development of a small number theory library, including in particular the solution to Pell's equation and properties of the Pell sequences.
Keywords
Cite
@article{arxiv.1802.01795,
title = {A Lean formalization of Matiyasevi\v{c}'s Theorem},
author = {Mario Carneiro},
journal= {arXiv preprint arXiv:1802.01795},
year = {2018}
}
Comments
6 pages