exlean: interactive theorem proving for mathematics education and research in Exeter

Recent posts

Groups I
Note: To follow along with this post create a new Lean file and …
Well-founded recursion
Abstract Well-founded recursion generalises both strong induction and recursion. In this post …

Mathematics in the 21st Century

Computer proof assistants aren’t new. One of the most popular provers, Coq, began development in 1984. However, they have mainly been the preserve of a select few logicians and computer scientists until recently. Leonardo de Moura is the principal architect of Lean, a new interactive theorem prover that has found widespread support from a community of mathematicians.

The blog articles on this website document attempts to understand, use, and teach Lean, and indeed to teach mathematics via Lean, at the University of Exeter.