Kevin Buzzard of Imperial College London joins Steven Strogatz to discuss Lean, formal proof assistants and the effort to encode mathematical knowledge in a computer-readable library. They explore how computers verify difficult arguments, the distinction between Lean and its mathematical library, the formalization of work by Peter Scholze and Dustin Clausen, and the prospects and limits of computers creating new mathematics.
In Computer Science and Mathematics