## Stream: general

### Topic: stacks project infrastructure

#### Kevin Buzzard (May 18 2020 at 16:03):

Back in 2018 Kenny and I formalised some tags in the stacks project, in a bad way. I am thinking of coming back to this project over the summer, but perhaps in a more sensible way. Let me just paint the most glorious picture I can imagine.

Say a Lean user is interested in a particular stacks project tag. Let's say for the sake of argument that it's a theorem, like tag 0052. Wouldn't it be great if there were some kind of repo/website/whatever, where they could type in the tag name, and it would say what has already been done with that tag from a Lean perspective. If the statement of the theorem is not formalised then there would be a way of letting a user upload a theorem statement, and if the proof is not formalised then there would be a way of letting a user upload a proof. I'm not expecting miracles, everything would have to be refereed, but just that basic infrastructure alone would perhaps be interesting to mathematicians who know some algebraic geometry and some Lean.

#### Patrick Massot (May 18 2020 at 16:05):

This would be easy to make. You only need to invest some time and energy.

#### Jalex Stark (May 18 2020 at 16:12):

Is the correct infrastructure just a copy of the stacks project where you sometimes add links to files or decls to a tag?

#### Kevin Buzzard (May 18 2020 at 16:27):

Yes, I think the chapters and sections should probably be preserved. One file per section maybe?

#### Johan Commelin (May 18 2020 at 16:48):

We could probably use something very similar to the 100.yaml that we're in the process of setting up.

Last updated: May 16 2021 at 21:11 UTC