exlean: interactive theorem proving for mathematics education and research in Exeter
Recent posts
Injectivity of succ
In the last post, I showed how to prove, using only elementary …
One of these things is not like the other
The simplest type type with a recursive constructor is the type of …
Categories
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.
