Links

Chat Room

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

Social Media

• The official Lean Twitter and Mastodon accounts.

Popular science articles about Lean

• Move Over, Mathematicians, Here Comes AlphaProof | The New York Times

• AI achieves silver-medal standard solving International Mathematical Olympiad problems | Google DeepMind

• DeepMind hits milestone in solving maths problems — AI’s next grand challenge | Nature.com

• The Deep Link Equating Math Proofs and Computer Programs | Quanta Magazine

• Why Mathematical Proof Is a Social Compact | Quanta Magazine

• A.I. Is Coming for Mathematics, Too | The New York Times

• How will AI change mathematics? Rise of chatbots highlights discussion | Nature.com

• "Lean" Computer Program Confirms Peter Scholze Proof | Quanta Magazine

• Will AI replace mathematicians? | Big Think

• Mathematicians welcome computer-assisted proof in ‘grand unification’ theory | Nature.com

• The Effort to Build the Mathematical Library of the Future | WIRED

Videos and Podcasts

• A.I.'s Mathematical Breakthrough interview with Pushmeet Kohli, Vice President, Research, Google DeepMind, on the New York Times Hard Fork podcast.

• Why Vlad Tenev and Tudor Achim of Harmonic Think AI Is About to Change Math discussion on Sequoia Capital's Training Data podcast.

• Terence Tao's Public Lecture about The Potential for AI in Science and Mathematics for Oxford Mathematics.

• Neha Rungta's talk on provably secure authorization, including references to Lean at AWS re:Inforce 2024.

• David Thrane Christiansen’s podcast #38 Haskell, Lean, Idris, and the Art of Writing on Type Theory Forall.

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