3
$\begingroup$

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.

Improve this question
$\endgroup$
16
  • 2
    $\begingroup$ How do you know that there are only two or three mistakes in the whole EGA's? $\endgroup$
    – Libli
    Commented Jun 8, 2019 at 13:33
  • $\begingroup$ @Libli well, I do not know for sure (I did say "maybe", hehe cunning me). I think there was one about formal smoothness, there was another one too which I can not remember. That should give a lower bound. Giving an upper bound depends on what sort of argument you are looking for (community consensus or something else). $\endgroup$
    – user141498
    Commented Jun 8, 2019 at 13:36
  • 3
    $\begingroup$ Well, what I wanted to say, is that I am not even sure that there is a group of scientists who has ever had the time and courage to read all the EGA line by line to check that validity of all statements. So, at least to me, it seems an impossible task for a group of scientists to formalize the EGA's in Lean. $\endgroup$
    – Libli
    Commented Jun 8, 2019 at 13:46
  • 1
    $\begingroup$ @Libli. Yes, I think that many students of the École Normale Supérieure have read all of EGA line by line: it has been some sort of challenge at that school for nearly 60 years and I guess that a couple of students each year manage to do just that. And mathematicians from other countries too: Deligne, Gabber, Suslin, Faltings, etc... Also, I don't see why it should take "courage" to read such a beautifully written, crystal clear , profound and epoch making treatise. $\endgroup$
    – Georges Elencwajg
    Commented Jun 9, 2019 at 20:10
  • 1
    $\begingroup$ Dear @Asura: let's say (to be on the safe side) that they finish reading all the volumes in a given year. On the other hand people like Deligne, Faltings and Gabber are rumored to have read EGA in about 6 months. I have heard that Jean-Charles Naouri quickly read all of EGA after being admitted to the ÉNS at the top of his cohort. He wrote his Ph.D. in one year but then (through lack of ambition ?) quit mathematics. He settled for a career as a businessman and his fortune is estimated at 0.5 billion euros. Sad story, eh? $\endgroup$
    – Georges Elencwajg
    Commented Jun 9, 2019 at 20:41

4 Answers 4

Reset to default
3
$\begingroup$

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.

Improve this answer
$\endgroup$
5
$\begingroup$

It's not clear whether which of the following you're most interested in:

  1. Formalizing EGA specifically.
  2. Formalizing in Lean specifically.
  3. 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.

Improve this answer
$\endgroup$
5
  • 1
    $\begingroup$ if the first paragraph was intended as a criticism of the question, I do not agree with it (there was only one sentence with a question mark, namely "Has EGA been translated into Lean or any other language aimed at formalizing mathematics? ", so I guess in your trichotomy that is 1). $\endgroup$
    – user141498
    Commented Jun 8, 2019 at 18:49
  • $\begingroup$ +1: a helpful answer, I appreciate the remark about the difficulty of formalizing EGA, I did not know that. $\endgroup$
    – user141498
    Commented Jun 8, 2019 at 18:50
  • 6
    $\begingroup$ The situation has improved in a number of ways since I wrote those slides. If you want to use Coq, there is now a single installer that will give you Coq + ssreflect + the mathematical components library, and the book (math-comp.github.io/mcb) by Mahboubi and Tassi is much better than previously available documentation. Lean also has more involvement of active mathematicians, and I think that the ecosystem works better than for other systems. It would be a lot of work to formalise EGA, but I would say that we know how to do it. $\endgroup$
    – Neil Strickland
    Commented Jun 9, 2019 at 8:32
  • 2
    $\begingroup$ @NeilStrickland It would be, I think, helpful to have a ballpark estimate for how much work would be involved to formalise EGA with presently available tools. Are we talking 1 person-month or 100 person-years? $\endgroup$
    – David Loeffler
    Commented Jun 9, 2019 at 13:39
  • 5
    $\begingroup$ @DavidLoeffler my guess would be 10 person-years. $\endgroup$
    – Neil Strickland
    Commented Jun 9, 2019 at 14:00
3
$\begingroup$

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.

Improve this answer
$\endgroup$
1
  • $\begingroup$ indeed, very interesting stuff. Unfortunately, I never received formal instruction in CS or AI so it will take me some time to learn all of the fancy terms. $\endgroup$
    – user141498
    Commented Jun 9, 2019 at 8:49
2
$\begingroup$

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

Improve this answer
$\endgroup$
8
  • 1
    $\begingroup$ it appears they are even going further: "We outline a program in the area of formalization of mathematics to automate theorem proving in algebra and algebraic geometry." They automate something we are struggling to do by hand in a single case! $\endgroup$
    – user141498
    Commented Jun 8, 2019 at 14:59
  • $\begingroup$ it also appears that we are using the phrase "large chunks of algebraic geometry presented in an accessible form" in different ways (Stacks project definitely not match my usage of this phrase). So I am not sure whom you are quoting. $\endgroup$
    – user141498
    Commented Jun 8, 2019 at 15:00
  • 1
    $\begingroup$ Why not? "The Stacks project is an ever growing open source textbook and reference work on algebraic stacks and the algebraic geometry needed to define them. [...] he aim is to build algebraic geometry and use this in laying the foundations for algebraic stacks. The theory of commutative algebra, schemes, varieties, and algebraic spaces forms an integral part of the Stacks project." They're really starting from the ground up; I refer you to e.g. stacks.math.columbia.edu/tag/006S (the definition of a sheaf on a topological space). $\endgroup$
    – David Loeffler
    Commented Jun 8, 2019 at 15:05
  • 4
    $\begingroup$ This answer is misleading. Last time I checked, they haven’t made meaningful progress after writing this very bold “outline of a program”. $\endgroup$
    – Piotr Achinger
    Commented Jun 8, 2019 at 15:38
  • 1
    $\begingroup$ I follow the advances in machine learning and formal theorem proving, and I think there is no chance of this project succeeding unless somebody invested literally a billion dollars in it. $\endgroup$
    – arsmath
    Commented Jun 8, 2019 at 19:37

You must log in to answer this question.