Ax-Grothendieck in Lean

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.