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.
Best Answer
Schemes have been formalized in Lean, with the aim of verifying formally some parts of the Stacks project: see here and here. They have schemes but I'm not sure they have morphisms of schemes yet. This should give you a feeling of the difficulty of the task.