A Formalization of All Notions in the Statement of a Theorem by Deligne

We present a partial formalization using the Lean 4 theorem prover of the statement of Deligne’s theorem on attaching a p-adic Galois representation to a weight k eigenform. The case of this theorem for \(k = 2\) is an important part of the Wiles/Taylor-Wiles proof of Fermat’s Last Theorem. The statement of Deligne’s theorem involves diverse mathematical notions like Galois representations and modular forms. Apart from some proof obligations in some of the definitions, all mathematical objects in the statement have been completely defined. In this paper we also locate this work on a lattice of notions of partial formalization, with full formalization at the top, and formalization in which not even all notions have been defined at the bottom.