List of things that still needs to be formalised?

Stream: new members

[Sayantan Majumdar]

Is there a place where one can find a list of theorems or topics that still needs to be formalised? I see a lot of papers claiming they are formalising the same topic.

[Scott Morrison]

Not really... Mathlib is the list of the 0.01% of mathematics that has been formalised! It would be nonsensical to list the complement. If you tell us about your mathematical interests we can probably help you understand where the boundary is in that area.

[Ruben Van de Velde]

That's a very optimistic percentage :)

[Ruben Van de Velde]

Still, I wonder if it would be productive to have a list of things that would be interesting to formalize and that seem to have their prerequisites done

[Bulhwi Cha]

@Sayantan Majumdar See https://leanprover-community.github.io/undergrad_todo.html.

[Yury G. Kudryashov]

Also, we should add more to this list: https://github.com/leanprover-community/mathlib4/issues?q=is%3Aissue+is%3Aopen+sort%3Aupdated-desc+label%3A%22good+first+issue%22