Resources
FEATURED VIDEOS
Building Better Systems Podcast
#14: Leo de Moura — Combining the Worlds of Automated and Interactive Theorem Proving In Lean
NEW PODCASTS
Haskell, Lean, Idris and the Art of Writing
#38: David Christiansen, his book Functional Programming in Lean and the Little Typer.
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 (nytimes.com)
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
FEATURED ARTICLES
Here are some of the most popular papers about Lean by Lean developers. For further publications about Lean, the mathlib library, and other formalizations in Lean, please visit the Lean community website or search Google Scholar.
PUBLICATIONS
To cite Lean in your academic paper, please reference the paper The Lean 4 Theorem Prover and Programming Language.
ACADEMIC CITATIONS