Nicolas

Stream: new members

[Nicolas Tessore]

Hi everyone :wave: I'm having fun learning lean at a very low level. I was wondering if there is still any "busywork" that needs to be added to mathlib, where a beginner could be useful while starting out.

[Kevin Buzzard]

busywork normally appears as one adds more things to the library, but it gets done all the time; the library is very fast-moving. It's not impossible that there are some freebies available though.

[Eric Wieser]

Probably 75% of my PRs are busywork!