  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.

Logic