EGA/SGA/stacks project?

Stream: mathlib4

[sparkwenc]

I wonder if there are attempts to import the whole EGA/SGA/stacks project into lean?

[Kevin Buzzard]

This material is being added slowly but surely, but not in a coherent way such as "today we do EGA1 section 4", or "today we do these stacks tags", so don't expect some kind of 1-1 correspondence between what's in mathlib and what's in these resources.

[sparkwenc]

Ah great! I just finished the "glimpse of Lean tutorial" and later found it actually much more daunting than I imagined to formalize some topic systematically and coherently after reading some codes of in mathlib4

[Kevin Buzzard]

Yes formalisation is much harder than you think. But it's possible. Two PhD students at Imperial formalised the definition of a stack in December as part of a computing project on our PhD program.

[Antoine Chambert-Loir]

The stacks project or EGA more or less assume more basic algebra than what mathlib knows. One should first incorporate Bourbaki's Algebra and Commutative algebra in full, which requires a lot of their General topology.

[Johan Commelin]

I think the stacks project covers most of the comm.alg that it needs, right?

[Kevin Buzzard]

Yes I think so, but EGA0 assumes more.

[sparkwenc]

Kevin Buzzard said:

Yes formalisation is much harder than you think. But it's possible. Two PhD students at Imperial formalised the definition of a stack in December as part of a computing project on our PhD program.

Yes I am feeling like being the very beginner learning how to use epsilon-delta in analysis. Another difficulty is that currently I can hardly reconstruct the math by reading a snippet of lean codes. Looks very different even after faithful translation.

[Johan Commelin]

Yes, the algebraic geometry part of mathlib has readability issues. I hope to spend a bunch of time thinking about how to solve that starting in April. (Bunch of deadlines in Feb/Mar)

[Antoine Chambert-Loir]

Johan Commelin said:

I think the stacks project covers most of the comm.alg that it needs, right?

No, I don't think so. Very “basic” stuff is not really done. Sometimes stated explicitly, sometimes not.

[Johan Commelin]

But I hope that this "basic" stuff is mostly done in mathlib already. But maybe I'm too optimistic.

[Adam Topaz]

How "basic" is the "basic" stuff?

[Adam Topaz]

I guess there's this: https://stacks.math.columbia.edu/tag/00AR

[Adam Topaz]

cf. number 73 :)

[Johan Commelin]

A quick skim of the list suggests to me that 73 is the only missing item.

[Adam Topaz]

Looks like it. And it would be quite a challenge to formalize 73 anyway

[Adam Topaz]

Actually, do we have 21 and 22?

[Andrew Yang]

We have docs#is_transcendence_basis but not transcendence degree.

[Adam Topaz]

do we have the exchange property for relative algebraic closure?

[Anatole Dedecker]

I think what Antoine refers to is that, even for things that we do have in Mathlib, some use cases turn out to be almost impossible. An example from this summer was some use case for extending the scalars of a tensor product from the right, and it turned out to be a nightmare, which is not yet solved I think. And of course, if you want to consider non-unital and non-commutative rings, you are in troubles…

[Andrew Yang]

Might be fun to take a comm. alg. textbook (maybe atiyah and macdonald) and map each proposition to a mathlib theorem

[Ruben Van de Velde]

I'm surprised I can't find anyone who's done it yet

[Kevin Buzzard]

Jujian has just done some stuff about 0-dimensional rings in A-M but he might not have PR'ed it yet.

[Antoine Chambert-Loir]

Andrew Yang said:

Might be fun to take a comm. alg. textbook (maybe atiyah and macdonald) and map each proposition to a mathlib theorem

Yes, but I recommend using Bourbaki which go farther and which will have to be implemented in a way or another.
Also: those guys have been quite careful about how to build a paper math library, and I don't know of similar efforts.

[Christian Merten]

Should the precise reference of the corresponding proposition in, say Bourbaki, be part of the mathlib docstring? If yes, in which format?

[Kevin Buzzard]

Patrick Massot you formalised reams of Bourbaki -- do you have an opinion?

[Patrick Massot]

We don't have a well-specified format. In particular those refs are not collected by our tooling. But I still think they are very useful.

[Patrick Massot]

And we should have more of them.

[Christian Merten]

Is it a goal to add support for references to the tooling? What are you thinking of in particular? I could imagine an expandable References (similar to Equations) in the docs, that is parsed from some refs syntax in the doc string with a link to the corresponding entry in docs/references.bib.

[Patrick Massot]

Ideally yes.