Undergrad math not in mathlib: Outdated?

[harahu]

Just noticed that the undergrad todo page hasn't been touched since last year. That surprises me given the amount of activity in mathlib in 2024. Is it still accurate?

[PatrickMassot]

Unfortunately very few people seem to care about this page when contributing or reviewing contributions. So yes, it is probably outdated. Improvements are very welcome. Some items are probably easy to knock off because there are simply there. Sometimes it would require writing a couple of Lean declarations to match the elementary setting of this list. There are also probably a number of middle size projects that would be great to have and fun to work on.

[harahu]

Improvements are very welcome.

I unfortunately can't help you here. I'm just an engineer with an outside-looking-in enthusiasm for what mathlib tries to achieve. Although I've dabbled with the Natural Number Game, my limited knowledge of both Lean and math curriculum means I'm far away from contributing effectively.

Just wanted to let you all know that as an outside observer wanting to update myself on mathlibs progress at a high level, the "Library overviews" pages are usually where I go. I know that I'm not the most important target audience to keep informed, and those already involved in the project probably stay sufficiently informed by following PRs and participating in discussions. But perhaps these pages, if kept up to date, could help lure in even more mathematical talent.

Having a clear and up-to-date overview of the delta between what "should" be in mathlib and what is in mathlib, could hopefully help motivate and guide work in addition to communicating outwards. Such an overview doesn't need to consist of these pages, though. It could also be something easier to maintain, like a GitHub project.

Finally I just want to say that I strongly believe you guys are laying the foundation for what will sooner or later become a revolution in mathematics. Keep up the good work. <3