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