PhD student interested in interactive theorem proving.