A Lean formalization of Matiyasevi\v{c}'s Theorem

TL;DR

This paper formalizes Matiyasevič's theorem within the Lean theorem prover, demonstrating the Diophantine nature of the power function and completing the proof of the MRDP theorem related to Hilbert's 10th problem.

Contribution

It provides a concise formalization of Matiyasevič's theorem in Lean, including new developments in number theory libraries like Pell's equation solutions.

Findings

Successful formalization of Matiyasevič's theorem in Lean

Development of number theory library components in Lean

Contribution to the proof of the MRDP theorem

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 $x,y$ sequences.