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

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!