A Lean formalization of Matiyasevič's Theorem
arXiv:1802.01795
Abstract
In this paper, we present a formalization of Matiyasevič'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.
6 pages