Formalising Families of \(\ell \) -adic Galois Representations in Lean 4

Families of \(\ell \) -adic Galois representations are an important tool in modern algebraic number theory. Andrew Wiles [1] used families of representations associated with elliptic curves to prove Fermat’s Last Theorem and the Langlands philosophy conjectures a deep connection to the theory of automorphic forms [2]. We formalise the definition of families of \(\ell \) -adic Galois representations as well as the definition of compatibility on them for the first time in an interactive theorem prover and discuss the formalisation process.