stacks project infrastructure

Stream: general

[Kevin Buzzard]

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]

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

[Jalex Stark]

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]

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

[Johan Commelin]

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