exlean: interactive theorem proving for mathematics education and research in Exeter
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.