Teaching Mathematics with Lean

This website is dedicated to collect education research activity regarding the use of automated theroem provers - and in particular Lean - for teaching undergraduate mathematics.

An Automated Theorem Prover is - according to Wiki - a software tool to assist with the development of formal proofs by human-machine collaboration. This involves some sort of interactive proof editor, or other interface, with which a human can guide the search for proofs, the details of which are stored in, and some steps provided by, a computer.

The interest in the use of these tools for teaching mathematics to first year students is growing fast. In this website we are interested in the educational outcomes of using these tools - which we will report on from our own research and those of others.

We will also collect here videos and other materials from meetings about usign Lean (or other Thereom Provers) to teach mathematics - see the page about the meeting on the 06.04.2022 at Loughbrough University.