Links

Chat Room

• A public chat room dedicated to Lean is open on Zulip.

Social Media

• The official Lean Twitter and Mastodon accounts.

• 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é Paris-Saclay) 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.

• Automated Mathematical Proofs - Computerphile

• 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.

• “Will Computers Outsmart Mathematicians?”.

• “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

• Real-time Robotics Control in the Lean Language

• OpenAI formal math

• Meta AI: Teaching AI advanced mathematical reasoning

Lean meetings

The community website hosts a list of upcoming and past events on Lean.