Is there an awesome-lean repository?

Stream: new members

[Andre Popovitch]

I want to see the coolest things people have done in lean, is there a repository for these? If not, please drop some links here and I'll make one

[Kevin Buzzard]

The community website leanprover-community.github.io contains a lot of mathematical work

[Patrick Massot]

See in particular https://leanprover-community.github.io/lean_projects.html

[Stuart Presnell]

And there's also https://leanprover-community.github.io/100.html which lists the progress that's been made on a set of 100 mathematical problems ranging from irrational (real.sqrt 2) to the independence of the Continuum Hypothesis.

[Patrick Massot]

Note this is a traditional list in the world of proof assistants that is much older then Lean, not what we think is important. See https://leanprover-community.github.io/mathlib-overview.html for what we feel is a nice presentation of the content of mathlib (my preceding link was about project other than mathlib, most often using mathlib).