Implementing Operads?

Stream: new members

[Eugene Rabinovich]

Hi All! I am a mathematician that is getting started with Lean. I worked through the Natural Number Game and am partway through the book Mathematics in Lean. My research worked with algebraic operads and I thought it would be interesting to implement the theory of Koszul duality of operads in Lean (basically going through the book by Loday-Vallette). Does anybody have a sense of how feasible this would be given the current state of Mathlib? If not, is there a more manageable sub-chunk of operad theory to work with?