Zulip Chat Archive

Stream: general

Topic: stacks project infrastructure


view this post on Zulip 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.

view this post on Zulip Patrick Massot (May 18 2020 at 16:05):

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

view this post on Zulip 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?

view this post on Zulip Kevin Buzzard (May 18 2020 at 16:27):

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

view this post on Zulip 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