The Lean theorem prover is a proof assistant developed principally by Leonardo de Moura at Microsoft Research.
There has been a community effort to develop mathlib, a library of mathematics formalized in Lean. This library also contains definitions useful for programming.
Much of the discussion surrounding Lean occurs in a Zulip chat room. Since this chatroom is only visible to registered users, we provide an openly accessible archive of the public discussions. This is useful for quick reference; for a better browsing interface, and to participate in the discussions, we strongly suggest joining the chat. Questions from users at all levels of expertise are welcomed.