complexity theory

Stream: maths

[Arthur Paulino]

I've searched through mathlib's branches and this was the only progress I could find under the scope of Complexity Theory, which has been inactive for over a year. Is there anyone else tackling this front at the moment?

[Scott Morrison]

I'm not sure if anyone is actively working on this. I agree it would be great to have some complexity theory in mathlib, just be warned it will require some subtle design decisions and may be difficult as a first project. I'd suggest posting early drafts here on zulip early on for feedback!

[Arthur Paulino]

Yeah that's what I thought too! I thought about complexity theory because it's a subject I am very interested in. But since I am still green on Lean, I totally agree that I should pick something slightly more constrained first. Thanks for the consideration!