Return to Answer

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 the 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.)

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.)

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 the any substantial chunk of algebraic geometry.)

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 the 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.)

Someone has already tried this: as a source for "large chunks of algebraic geometry presented in an accessible form" 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.

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 the any substantial chunk of algebraic geometry.)