I have been lately thinking about the feasibility of creating a "mediocre algebraic geometer" AI. I thought that to train it, one could feed it some large chunks of algebraic geometry presented in an accessible form.

I do not think that human-written text counts as an accessible form, even one using very limited number of words so it would be less headache if it was written in a formal logic language (I think Lean has sufficient functionality for this, for example).

Has EGA been translated into Lean or any other language aimed at formalizing mathematics? Given that EGA was written pretty transparently (and there were very few errors for a text of this length, two or three maybe), it should not be excessively hard to do this but it can require quite some time to translate all the volumes.