My masters project was formalizing the model theoretic proof of Ax-Grothendieck in Lean. My repository for the Lean code can be found here and my paper and presentation on the subject can both be found here.