Chat Room
 A public chat room dedicated to Lean is open on Zulip.
Social Media

Kevin Buzzard’s @xenaproject Mastodon account about Lean.
Popular science articles about Lean

The Deep Link Equating Math Proofs and Computer Programs Another Quanta article that mentions Lean.

Why Mathematical Proof Is a Social Compact A Quanta article that mentions Lean, and the accompanying video shows Lean code.

New York Time’s article “A.I. Is Coming for Mathematics, Too” cites Lean and some of its projects.

Nature’s article “How will AI change mathematics?” cites Lean multiple times.

Wired article about the Lean mathematical library.

Nature’s article about Peter Scholze’s (Fields Medal in 2018) project formalized in Lean.

Jordan Ellenberg’s article mentioning Scholze’s result and Lean.

Can Computers be Mathematicians, The Joy of Why, Quanta Magazine podcast.

Proof Assistant Makes Jump to Big League Math, Quanta article about Scholze’s result and Lean.

Quanta article about the IMO grand challenge.

Lean has been mentioned in Quanta’s The Year in Math and Computer Science two years in a row: 2020 and 2021.
Videos and Podcasts

Z3 and Lean, the Spiritual Journey at the Type Theory Forall podcast.

Lean 4: Empowering the Formal Mathematics Revolution and Beyond presented by Leonardo de Moura (Amazon Web Services) at the Topos Institute Colloquium organised by the Topos Institute.

The Lean Proof Assistant: Introduction and Challenges presented by Leonardo de Moura (Microsoft Research) at the Machine Assisted Proofs Workshop organised by the Institute for Pure & Applied Mathematics (IPAM) of UCLA.

Formal Mathematics for Mathematicians and Mathematics Students presented by Patrick Massot (Université ParisSaclay) at the Machine Assisted Proofs Workshop organised by the Institute for Pure & Applied Mathematics (IPAM) of UCLA.

Formalizing Invisible Mathematics presented by Andrej Bauer (University of Ljubljana) at the Machine Assisted Proofs Workshop organised by the Institute for Pure & Applied Mathematics (IPAM) of UCLA.

Learning Mathematics with Lean (2022): playlist containing the recorded talks of the first Learn Mathematics with Lean event (06/04/2022) organised by the Department of Mathematics Education of the Loughborough University.

The rise of formalism in mathematics, Kevin Buzzard’s invited talk at ICM 2022.

Charles Hoskinson talking about the Hoskinson Center for Formal Mathematics and Lean.

Jeremy Avigad at the opening of the Hoskinson Center at Carnegie Mellon University

Combining the Worlds of Automated and Interactive Theorem Proving In Lean at the Building Better Systems podcast.

A collection of YouTube videos about Lean created by the community.

Lean mathematical library is one of Quanta magazine’s “2020’s Biggest Breakthroughs in Math and Computer Science”.

“The future of mathematics?” by Kevin Buzzard.

Podcast with Alex Kontorovich where he talks about Lean.

“The Dawn of Formalized Mathematics”, by Andrej Bauer. It also includes this video showing activities of mathematicians working on the Lean mathematical library.
Blog posts
Lean meetings
The community website hosts a list of upcoming and past events on Lean.