A complete formalization of EGA in Lean 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.
 A: It's not clear whether which of the following you're most interested in:


*

*Formalizing EGA specifically.

*Formalizing in Lean specifically.

*Teaching an AI to do mathematics by giving it a bunch of formalized mathematics and waving a magic wand while muttering the magic spell "deep learning."


Questions 1 and 2 are relatively easy to answer.  Nobody has formalized EGA in Lean or any other proof assistant.  I think you overestimate how easy it is to formalize significant amounts of mathematics using a proof assistant.  I recommend that you look through the slides of a talk by Neil Strickland, Proof assistants as a routine tool? to get a sense of where the state of the art is.  (Strickland's slides were written a while ago but the current situation is still mostly as he described it.)  Until it gets a lot easier to use proof assistants, formalizing EGA is unlikely to happen.
As for Question 3, the idea has long been at the back of the minds of many people who work with formal proofs.  While I think the time is not yet ripe for such a project, there's no harm in trying.  But if you do want to try, and if you don't have your heart set on algebraic geometry per se, it probably makes sense to pick some area of mathematics that has already been formalized to a significant extent, rather than start from scratch.  For example you could try to join the univalent foundations / homotopy type theory community.
A: 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.
A: You might be interested in the Lean Forward project (https://lean-forward.github.io/).  This is in number theory rather than algebraic geometry, but it is probably the largest and most well organised current project aiming to apply formalisation to current research.
For applications of AI to this area, here are two abstracts from the Big Proof 2019 meeting in Edinburgh: 

Saxton, David (DeepMind)
Teaching machines to do mathematics like humans 
Can we teach machines
  to do mathematics following the same curriculum that we use for
  humans? We released a dataset of synthetic school level mathematical
  questions - what happens when we try to train standard
  state-of-the-art learning models (without any prior mathematical
  knowledge) to answer these? (Spoiler: they can do well on many but not
  all problem types - and their perceptual reasoning process is still a
  long way off from the power of humans.) We also look at motivations
  for doing this, and speculate on what next steps might be for learning
  models that could do harder mathematics (perhaps eventually things
  like conjectures and proofs) in a human-like fashion.

.

Urban, Josef (Prague)
Learning and Reasoning over Big Proof Corpora
The talk
  will give a brief overview of recent methods that combine learning and
  reasoning over large formal libraries. I will mention the "hammer"
  linkups between ITPs and ATPs, systems that learn and perform direct
  tactical guidance of ITPs, discuss learning of premise selection over
  large libraries and learning-based guidance of saturation-style and
  tableaustyle automated theorem provers (ATPs) trained over the large
  proof corpora. I will also mention feedback loops between proving and
  learning in this setting, and show our auto formalization experiments.

A: Someone has already tried this: as a source for "large chunks of algebraic geometry" they used the Stacks Project. You can read more about the results here:
Chojecki, P. (2017), DeepAlgebra - An Outline of a Program. In: Geuvers H., England M., Hasan O., Rabe F., Teschke O. (eds), Intelligent Computer Mathematics - CICM 2017, Lecture Notes in Computer Science, vol 10383, Springer.
(EDIT, in response to comments: The emphasis here is on tried. I did not claim that this programme had already succeeded in creating a formalization of any substantial chunk of algebraic geometry. The programme proposed by Chojecki also differs from the context of the question in that -- if I understand correctly -- Chojecki proposes to train an AI directly on the natural-language text of the Stacks Project, while the questioner proposes to have humans rewrite EGA in a formal language and then use that to train an AI.)
