Stream: Archive Mirror: Isabelle Users Mailing List

Topic: [isabelle] Interactive theorem proving: 3 Postdoctoral po...


view this post on Zulip Email Gateway (Aug 22 2022 at 15:32):

From: Lawrence Paulson <lp15@cam.ac.uk>
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:

http://www.jobs.cam.ac.uk/job/13866/
http://www.jobs.cam.ac.uk/job/13867/

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


Last updated: Apr 25 2024 at 12:23 UTC