Virtual Talk: The Lean proof assistant: introduction and challenges

Leonardo de Moura
Microsoft Research

Lean is the proof assistant of choice for the mathematics community.
It is also an efficient programming language, and users can extend Lean functionality using Lean itself.
The Lean mathematical library (Mathlib) has more than one million lines of code and contributions from more than 200 people.
This talk briefly introduces the Lean proof assistant and discusses the many challenges ahead.

Back to Machine Assisted Proofs