Formalizing computability theory via partial recursive functions

We present an extension to the $\mathtt{m}\mathtt{a}\mathtt{t}\mathtt{h}\mathtt{l}\mathtt{i}\mathtt{b}$ library of the Lean theorem prover formalizing the foundations of computability theory. We use primitive recursive functions and partial recursive functions as the main objects of study, and we use a constructive encoding of partial functions such that they are executable when the programs in question provably halt. Main theorems include the construction of a universal partial recursive function and a proof of the undecidability of the halting problem. Type class inference provides a transparent way to supply G"{o}del numberings where needed and encapsulate the encoding details.