More Project ideas

Stream: Berkeley Lean Seminar

[Kevin Buzzard]

I've been talking to Pieter Belmans about adding a "this tag formally verified by Lean!" functionality to the stacks project. Scott Morrison has been going through mathlib tagging stuff with stacks tags. There's a general commutative algebra overview tag which we seem to be inadvertantly working through. If people here want to do some more commutative algebra after FTG (which I'm assuming is the goal of the other projects) then this https://stacks.math.columbia.edu/tag/00AO is what we're aiming at.