exlean: interactive theorem proving for mathematics education and research in Exeter
Recent posts
Announcing a one-day workshop in interactive theorem proving in education and research July 2024
Workshop announcement On 24 July 2024, the University of Exeter is hosting …
Lean 3 & the new elan on ARM Mac
Of course, Lean 3 is now deprecated. But you may still want …
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.