Developing euclidean domains and the isomorphism theorems for groups in Lean, an interactive theorem prover

Date & time

3–4.30pm 16 February 2018


John Dedman Building 27, Room JD1177 (meeting room)


Mitchell Rowett and Louis Carlin (ANU)


 Scott Morrison

Summer ASC students Louis Carlin and Mitchell Rowett will describe their experience developing mathematical libraries for Lean, a new interactive theorem prover. Mitchell has been working on developing basic group theory, including some of the isomorphism theorems. Louis has been developing euclidean domains, including the euclidean algorithm. It turns out there's an interesting subtlety in the induction step of the euclidean algorithm, which is easy for human mathematicians to overlook!

Updated:  21 April 2018/Responsible Officer:  Director/Page Contact:  School Manager