The Lean Proof Assistant and Programming Language Resource Guide

Popular science articles

• A.I. Is Coming for Mathematics, Too, New York Times article. (archive link)
• How will AI change mathematics?, Nature news article. (archive link)
• The Effort to Build the Mathematical Library of the Future, Wired article about the Lean mathematical library.
• Why Mathematical Proof Is a Social Compact, Quanta article mentioning Lean, video.
• Mathematicians welcome computer-assisted proof in ‘grand unification’ theory, Nature news article about the Liquid Tensor experiment where Lean was used to verify Peter Scholze’s latest result, Fields Medal 2018. (archive link)
• Proof Assistant Makes Jump to Big-League Math, Quanta article about the Liquid Tensor experiment.
• Lean has been mentioned in Quanta’s The Year in Math and Computer Science two years in a row: 2020 and 2021.
• Will AI replace mathematicians?, Jordan Ellenberg’s article at Big Think.
• The Deep Link Equating Math Proofs and Computer Programs, Quanta article that mentions Lean.
• ‘A-Team’ of Math Proves a Critical Link Between Addition and Sets. Quanta article that mentions Lean.

External AI efforts based on Lean

• OpenAI: Solving (some) formal math olympiad problems. (paper)
• Meta AI: Teaching AI advanced mathematical reasoning. (paper)
• LeanDojo: open source models, datasets, and code for Lean. (paper, video)
• xAI: adding support for Lean to Grok.
• Morph labs: developing ML models for Lean and moogle.ai, an AI for searching the Lean mathematical library using natural language.
• DeepMind: They have formalized a result related to AI safety in Lean. (paper, code)

Tools for controlling and extracting data from Lean

• Read-eval-print-loop via Json messages: https://github.com/leanprover-community/repl
• Extracting data: https://github.com/semorrison/lean-training-data

Social media

• Twitter: https://twitter.com/leanprover
• LinkedIn: https://www.linkedin.com/company/lean-fro
• Mastodon: https://functional.cafe/@leanprover
• Tim Gowers on Lean, Fields Medalist 1998.
• Terence Tao posting that he decided to learn Lean, Fields Medal 2006. He used Lean to find a bug in one his papers. Tao’s blog post on the PFR project using Lean.
• Interview with Peter Scholze, Fields Medal 2018.

Books and manuals

• Functional Programming in Lean
• The Mechanics of Proof
• Mathematics in Lean
• Theorem Proving in Lean 4
• Metaprogramming in Lean 4
• Reference Manual (work in progress)
• How to Prove it with Lean, based on the textbook How To Prove It: A Structured Approach, 3rd edition

Websites

• Homepage: https://lean-lang.org
• Web editor (try Lean in your web browser): https://live.lean-lang.org
• Lean nonprofit: https://lean-fro.org
• Lean community website: https://leanprover-community.github.io
• Main libraries documentation: https://leanprover-community.github.io/mathlib4_docs
• Loogle (search libraries online): https://loogle.lean-lang.org
• Reservoir (package repository, work in progress): https://reservoir.lean-lang.org
• Discussion channel: https://leanprover.zulipchat.com
• Upcoming and past Lean-related events and conferences: https://leanprover-community.github.io/events.html

Videos and podcasts

• Machine-Checked Proofs and the Rise of Formal Methods in Mathematics at Simons Institute, October 2023
• The Rise of Formalism in Mathematics, by Kevin Buzzard at ICML 2022.
• Hoskinson Center for Formal Mathematics at CMU, Charles Hoskinson, 2021.
• Jeremy Avigad at the opening of the Hoskinson Center at CMU, 2021.
• Automated Mathematical Proofs - Computerphile.
• Z3 and Lean, the Spiritual Journey, Type Theory Forall podcast.
• The Future of Mathematics?, by Kevin Buzzard at MSR
• Combining the Worlds of Automated and Interactive Theorem Proving in Lean, Building Better Systems podcast.
• The Lean nonprofit YouTube channel.
• The Lean community YouTube channel.