[FOM] Interactive theorem proving: 3 Postdoctoral positions at Cambridge

Lawrence Paulson lp15 at cam.ac.uk
Fri May 26 11:43:25 EDT 2017

ALEXANDRIA is a five-year ERC-funded project aimed at making interactive theorem proving useful in mathematical research. The workplan includes pilot studies to identify critical issues, library development and the implementation of advanced search, perhaps using machine learning. Two mathematicians and an Isabelle architect will be hired. Official descriptions of the vacancies are online:


We can look forward to some exciting developments! And while this project will be based on Isabelle, I also hope for fruitful cooperation with users of other systems.

Larry Paulson

Computer Laboratory, University of Cambridge
Cambridge CB3 0FD, England
Tel: +44(0)1223 334623   


More information about the FOM mailing list